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

Theorem bicom 213
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 212 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 212 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 200 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  bicomd  214  bibi1i  329  bibi1d  334  con2bi  344  ibibr  359  bibif  362  nbbn  374  pm5.17  1035  biluk  1050  bigolden  1051  xorcom  1636  trubifal  1684  euae  2683  abeq1  2876  ssequn1  3947  axpow3  5006  isocnv  6774  qextlt  12239  qextle  12240  rpnnen2lem12  15239  odd2np1  15350  sumodd  15396  nrmmetd  22661  lgsqrmodndvds  25372  cvmlift2lem12  31747  nn0prpw  32764  bj-abeq1  33207  tsbi4  34367  bicomdd  34812  ifpbicor  38499  rp-fakeoranass  38538  or3or  38996  3impexpbicom  39360  3impexpbicomVD  39748  limsupreuz  40610  nabctnabc  41741
  Copyright terms: Public domain W3C validator