Theorem bicom 225

Description: Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)

Assertion

Ref	Expression
bicom	⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		bicom1 224	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
2		bicom1 224	. 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
3	1, 2	impbii 212	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicomd  226  bibi1i  341  bibi1d  346  con2bi  356  ibibr  371  bibif  374  nbbnOLD  387  birot  389  biluk  390  biadan  831  pm5.17  1029  bigolden  1044  xorcom  1544  norass  1567  trubifal  1601  hadcoma  1629  eqabcbw  2838  eqabcb  2904  pm13.183  3623  ssequn1  4187  isocnv  7358  qextlt  13357  qextle  13358  rpnnen2lem12  16419  odd2np1  16537  sumodd  16584  nrmmetd  24920  lgsqrmodndvds  27707  eqelbid  33140  mgccnv  33627  cvmlift2lem12  36245  nn0prpw  37288  wl-3xorrot  38591  wl-3xorcoma  38592  tsbi4  39259  bicomdd  40102  onsupmaxb  44431  ifpbicor  44666  rp-fakeoranass  44705  or3or  45213  3impexpbicom  45652  3impexpbicomVD  46028  notbicom  46383  limsupreuz  46950  nabctnabc  48204