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  700  con2bidc  877  con2biddc  882  pm5.17dc  906  bigolden  958  nbbndc  1414  bilukdc  1416  falbitru  1437  3impexpbicom  1458  exists1  2150  eqcom  2207  abeq1  2315  necon2abiddc  2442  necon2bbiddc  2443  necon4bbiddc  2450  ssequn1  3343  axpow3  4221  isocnv  5880  suplocsrlem  7921  uzennn  10581  bezoutlemle  12329