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  687  con2bidc  860  con2biddc  865  pm5.17dc  889  bigolden  939  nbbndc  1372  bilukdc  1374  falbitru  1395  3impexpbicom  1414  exists1  2093  eqcom  2139  abeq1  2247  necon2abiddc  2372  necon2bbiddc  2373  necon4bbiddc  2380  ssequn1  3241  axpow3  4096  isocnv  5705  suplocsrlem  7609  uzennn  10202  bezoutlemle  11685