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  biluk  389  biadan  830  pm5.17  1028  bigolden  1043  xorcom  1543  norass  1566  trubifal  1600  hadcoma  1628  eqabcbw  2836  eqabcb  2902  pm13.183  3624  ssequn1  4138  isocnv  7328  qextlt  13235  qextle  13236  rpnnen2lem12  16287  odd2np1  16405  sumodd  16452  nrmmetd  24742  lgsqrmodndvds  27528  eqelbid  32832  mgccnv  33328  cvmlift2lem12  35814  nn0prpw  36862  wl-3xorrot  38151  wl-3xorcoma  38152  tsbi4  38813  bicomdd  39656  onsupmaxb  43994  ifpbicor  44229  rp-fakeoranass  44268  or3or  44777  3impexpbicom  45217  3impexpbicomVD  45593  notbicom  45911  limsupreuz  46479  nabctnabc  47696