Theorem pm5.21 676

Description: Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124.

Assertion

Ref	Expression
pm5.21	|- ((-. ph /\ -. ps) -> (ph <-> ps))

Proof of Theorem pm5.21

Step	Hyp	Ref	Expression
1		pm5.1 675	. 2 |- ((-. ph /\ -. ps) -> (-. ph <-> -. ps))
2	1	con4bid 523	1 |- ((-. ph /\ -. ps) -> (ph <-> ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm5.21ni 677  pm5.21nd 679  bibif 680  2false 718  nbn2 720  fn0 3597  eqfnfv 3788  eceqopreq 4303  ixp0 4351  axrepnd 4926  lt2msq 5837  nn0ltp1let 6082  zltp1let 6136  elcncf 7208  znnenlemOLD 7452

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain