Theorem bicom 139

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 130	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
2		bicom1 130	. 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
3	1, 2	impbii 125	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicomd  140  bibi1i  227  bibi1d  232  ibibr  245  bibif  693  con2bidc  870  con2biddc  875  pm5.17dc  899  bigolden  950  nbbndc  1389  bilukdc  1391  falbitru  1412  3impexpbicom  1431  exists1  2115  eqcom  2172  abeq1  2280  necon2abiddc  2406  necon2bbiddc  2407  necon4bbiddc  2414  ssequn1  3297  axpow3  4163  isocnv  5790  suplocsrlem  7770  uzennn  10392  bezoutlemle  11963