Theorem bicom 398

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

Assertion

Ref	Expression
bicom	⊢ ((φ ↔ ψ) ↔ (ψ ↔ φ))

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		ancom 333	. 2 ⊢ (((φ → ψ) ∧ (ψ → φ)) ↔ ((ψ → φ) ∧ (φ → ψ)))
2		bi 396	. 2 ⊢ ((φ ↔ ψ) ↔ ((φ → ψ) ∧ (ψ → φ)))
3		bi 396	. 2 ⊢ ((ψ ↔ φ) ↔ ((ψ → φ) ∧ (φ → ψ)))
4	1, 2, 3	3bitr4 158	1 ⊢ ((φ ↔ ψ) ↔ (ψ ↔ φ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  bicomd 399  pm4.11 400  bibi1i 461  bibi1d 471  oibabs 493  pm5.18 497  nbbn 498  biluk 512  bigolden 513  sbequ12r 866  exists1 1072  cleqcom 1103  cleqabr 1175  isocnv 2934

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org