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  699  con2bidc  876  con2biddc  881  pm5.17dc  905  bigolden  957  nbbndc  1405  bilukdc  1407  falbitru  1428  3impexpbicom  1449  exists1  2138  eqcom  2195  abeq1  2303  necon2abiddc  2430  necon2bbiddc  2431  necon4bbiddc  2438  ssequn1  3330  axpow3  4207  isocnv  5855  suplocsrlem  7870  uzennn  10510  bezoutlemle  12148