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

Theorem bicom 211
 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 210 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 210 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 198 1 ((𝜑𝜓) ↔ (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195 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 196 This theorem is referenced by:  bicomd  212  bibi1i  327  bibi1d  332  con2bi  342  ibibr  357  bibif  360  nbbn  372  pm5.17  928  biluk  970  bigolden  972  xorcom  1459  trubifal  1513  exists1  2549  abeq1  2720  ssequn1  3745  axpow3  4772  isocnv  6480  qextlt  11908  qextle  11909  rpnnen2lem12  14793  odd2np1  14903  sumodd  14949  nrmmetd  22189  lgsqrmodndvds  24878  cusgrauvtxb  26024  cvmlift2lem12  30550  nn0prpw  31488  bj-abeq1  31962  tsbi4  33113  bicomdd  33153  ifpbicor  36839  rp-fakeoranass  36878  or3or  37339  3impexpbicom  37706  3impexpbicomVD  38114  nabctnabc  39747
 Copyright terms: Public domain W3C validator