Theorem pm5.1 675

Description: Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123.

Assertion

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

Proof of Theorem pm5.1

Step	Hyp	Ref	Expression
1		pm5.501 594	. 2 |- (ph -> (ps <-> (ph <-> ps)))
2	1	biimpa 416	1 |- ((ph /\ ps) -> (ph <-> ps))

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

This theorem is referenced by:  pm5.21 676  pm5.35 681  pm5.54 682  sbc2or 1954  ssconb 2166  ralidm 2353  raaan 2356  cnvpo 3514  eceqopreq 4303  sucdom 4822  zltp1let 6136  sqlecant 6580  znnenlem 7451  mdsym 10275

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