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  688  con2bidc  865  con2biddc  870  pm5.17dc  894  bigolden  945  nbbndc  1384  bilukdc  1386  falbitru  1407  3impexpbicom  1426  exists1  2110  eqcom  2167  abeq1  2276  necon2abiddc  2402  necon2bbiddc  2403  necon4bbiddc  2410  ssequn1  3292  axpow3  4156  isocnv  5779  suplocsrlem  7749  uzennn  10371  bezoutlemle  11941