Theorem bicom 140

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bicomd  141  bibi1i  228  bibi1d  233  ibibr  246  bibif  698  con2bidc  875  con2biddc  880  pm5.17dc  904  bigolden  955  nbbndc  1394  bilukdc  1396  falbitru  1417  3impexpbicom  1438  exists1  2122  eqcom  2179  abeq1  2287  necon2abiddc  2413  necon2bbiddc  2414  necon4bbiddc  2421  ssequn1  3307  axpow3  4179  isocnv  5814  suplocsrlem  7809  uzennn  10438  bezoutlemle  12011