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 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bicomd  141  bibi1i  228  bibi1d  233  ibibr  246  bibif  710  con2bidc  887  con2biddc  892  pm5.17dc  916  bigolden  968  nbbndc  1443  bilukdc  1445  falbitru  1466  3impexpbicom  1488  exists1  2183  eqcom  2240  abeq1  2348  eqabcbw  2376  eqabcb  2377  necon2abiddc  2486  necon2bbiddc  2487  necon4bbiddc  2494  ssequn1  3399  axpow3  4314  isocnv  6017  suplocsrlem  8175  uzennn  10873  bezoutlemle  12785