Exercise logic.propositional.consequence

Description
Prove that formula is a logical consequence of a set of formulas

All applications

• Rule	conj-intro
  Location	[]

  

  (p <-> q) /\ ~p => ~q

  ready: no

• Rule	introfalseleft
  Location	[0,0]

  

  F || (p <-> q), ~p => ~q

  ready: no

• Rule	introfalseleft
  Location	[0,0,0]

  

  (F || p) <-> q, ~p => ~q

  ready: no

• Rule	introfalseleft
  Location	[0,0,1]

  

  p <-> (F || q), ~p => ~q

  ready: no

• Rule	introfalseleft
  Location	[0,1]

  

  p <-> q, F || ~p => ~q

  ready: no

• Rule	introfalseleft
  Location	[0,1,0]

  

  p <-> q, ~(F || p) => ~q

  ready: no

• Rule	introfalseleft
  Location	[1]

  

  p <-> q, ~p => F || ~q

  ready: no

• Rule	introfalseleft
  Location	[1,0]

  

  p <-> q, ~p => ~(F || q)

  ready: no

• Rule	logic.propositional.defequiv
  Location	[0,0]

  

  (p /\ q) || (~p /\ ~q), ~p => ~q

  ready: no