Theorem bicom 519

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 435	. 2 ⊢ (((φ → ψ) ⋀ (ψ → φ)) ↔ ((ψ → φ) ⋀ (φ → ψ)))
2		bi 514	. 2 ⊢ ((φ ↔ ψ) ↔ ((φ → ψ) ⋀ (ψ → φ)))
3		bi 514	. 2 ⊢ ((ψ ↔ φ) ↔ ((ψ → φ) ⋀ (φ → ψ)))
4	1, 2, 3	3bitr4 183	1 ⊢ ((φ ↔ ψ) ↔ (ψ ↔ φ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  bicomd 520  pm4.11 521  ibibr 590  bibi1i 608  bibi1d 618  pm5.18 659  nbbn 660  pm5.17 667  pm5.55 674  tbt 719  nbn 721  biluk 744  bigolden 746  sbequ12r 1180  exists1 1455  eqcom 1474  abeq1 1566  isocnv 3887  difeqri2 10380

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