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  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  4309  isocnv  6007  suplocsrlem  8165  uzennn  10851  bezoutlemle  12763