MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicom Structured version   Visualization version   GIF version

Theorem bicom 223
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
StepHypRef Expression
1 bicom1 222 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 222 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 210 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  bicomd  224  bibi1i  340  bibi1d  345  con2bi  355  ibibr  370  bibif  373  nbbn  385  biluk  387  biadan  815  pm5.17  1005  bigolden  1020  xorcom  1498  norass  1524  trubifal  1559  hadcoma  1590  abeq1  2946  ssequn1  4155  axpow3  5261  isocnv  7072  qextlt  12586  qextle  12587  rpnnen2lem12  15568  odd2np1  15680  sumodd  15729  nrmmetd  23113  lgsqrmodndvds  25857  cvmlift2lem12  32459  nn0prpw  33569  tsbi4  35297  bicomdd  35872  ifpbicor  39721  rp-fakeoranass  39760  or3or  40251  3impexpbicom  40693  3impexpbicomVD  41071  limsupreuz  41898  nabctnabc  43048  isomuspgrlem2b  43841
  Copyright terms: Public domain W3C validator