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 657  nbbn 658  pm5.17 665  pm5.55 672  tbt 717  nbn 719  biluk 742  bigolden 744  sbequ12r 1165  exists1 1434  eqcom 1453  abeq1 1545  isocnv 3835  difeqri2 8703

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