Theorem bicom 138

Description: Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 11-Nov-2012.)

Assertion

Ref	Expression
bicom	⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		bicom1 129	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
2		bicom1 129	. 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
3	1, 2	impbii 124	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Syntax hints:   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bicomd  139  bibi1i  226  bibi1d  231  ibibr  244  bibif  646  con2bidc  802  con2biddc  807  pm5.17dc  843  bigolden  896  nbbndc  1325  bilukdc  1327  falbitru  1348  3impexpbicom  1367  exists1  2037  eqcom  2083  abeq1  2188  necon2abiddc  2311  necon2bbiddc  2312  necon4bbiddc  2319  ssequn1  3142  axpow3  3951  isocnv  5471  bezoutlemle  10397