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

Theorem bicom 212
 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 211 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 211 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 199 1 ((𝜑𝜓) ↔ (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196 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 197 This theorem is referenced by:  bicomd  213  bibi1i  327  bibi1d  332  con2bi  342  ibibr  357  bibif  360  nbbn  372  pm5.17  968  biluk  1012  bigolden  1014  xorcom  1604  trubifal  1659  exists1  2687  abeq1  2859  ssequn1  3914  axpow3  4983  isocnv  6731  qextlt  12198  qextle  12199  rpnnen2lem12  15124  odd2np1  15238  sumodd  15284  nrmmetd  22551  lgsqrmodndvds  25248  cvmlift2lem12  31574  nn0prpw  32595  bj-abeq1  33051  tsbi4  34225  bicomdd  34611  ifpbicor  38291  rp-fakeoranass  38330  or3or  38790  3impexpbicom  39156  3impexpbicomVD  39560  limsupreuz  40441  nabctnabc  41573
 Copyright terms: Public domain W3C validator