Theorem bicom 518

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 435	. 2 |- (((ph -> ps) /\ (ps -> ph)) <-> ((ps -> ph) /\ (ph -> ps)))
2		bi 513	. 2 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
3		bi 513	. 2 |- ((ps <-> ph) <-> ((ps -> ph) /\ (ph -> ps)))
4	1, 2, 3	3bitr4 183	1 |- ((ph <-> ps) <-> (ps <-> ph))

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

This theorem is referenced by:  bicomd 519  pm4.11 520  ibibr 589  bibi1i 607  bibi1d 617  pm5.18 658  nbbn 659  pm5.17 666  pm5.55 673  tbt 718  nbn 720  biluk 743  bigolden 745  sbequ12r 1178  exists1 1450  eqcom 1469  abeq1 1561  isocnv 3881  difeqri2 10344

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