Theorem bicom 579

Description: Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117.

Assertion

Ref	Expression
bicom	|- ((ph <-> ps) <-> (ps <-> ph))

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		ancom 482	. 2 |- (((ph -> ps) /\ (ps -> ph)) <-> ((ps -> ph) /\ (ph -> ps)))
2		dfbi2 572	. 2 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
3		dfbi2 572	. 2 |- ((ps <-> ph) <-> ((ps -> ph) /\ (ph -> ps)))
4	1, 2, 3	3bitr4i 200	1 |- ((ph <-> ps) <-> (ps <-> ph))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  bicomd 580  notbi 581  ibibr 651  bibi1i 671  bibi1d 681  pm5.18OLD 723  nbbn 724  pm5.17 731  pm5.55 739  tbtOLD 789  nbn 791  biluk 817  bigolden 819  3impexpbicom 1287  sbequ12rOLD 1547  exists1 1862  eqcom 1886  abeq1 2000  ssequn1 2775  axpow3 3484  isocnv 4873  bnj926 12832  bnj1130 12933  FTBid 14122  bicomdd 16228  compne 16417  3impexpbicomVD 16681

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 164  df-an 242

Copyright terms: Public domain