Theorem bicom 224

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 223	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
2		bicom1 223	. 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
3	1, 2	impbii 211	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Syntax hints:   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  bicomd  225  bibi1i  340  bibi1d  345  con2bi  355  ibibr  370  bibif  373  nbbnOLD  386  biluk  388  biadan  828  pm5.17  1025  bigolden  1040  xorcom  1536  norass  1559  trubifal  1593  hadcoma  1621  eqabcbw  2838  eqabcb  2904  pm13.183  3627  ssequn1  4140  isocnv  7316  qextlt  13208  qextle  13209  rpnnen2lem12  16259  odd2np1  16377  sumodd  16424  nrmmetd  24636  lgsqrmodndvds  27419  eqelbid  32676  mgccnv  33179  cvmlift2lem12  35669  nn0prpw  36688  wl-3xorrot  37976  wl-3xorcoma  37977  tsbi4  38640  bicomdd  39483  onsupmaxb  43821  ifpbicor  44056  rp-fakeoranass  44095  or3or  44604  3impexpbicom  45061  3impexpbicomVD  45437  notbicom  45748  limsupreuz  46316  nabctnabc  47530