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

Theorem bicom 203
Description: Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)
Assertion
Ref Expression
bicom  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )

Proof of Theorem bicom
StepHypRef Expression
1 bicom1 202 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 202 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 190 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  bicomd  204  bibi1i  315  bibi1d  320  con2bi  329  ibibr  344  bibif  347  nbbn  359  pm5.17  896  biluk  941  bigolden  943  bianirOLD  976  xorcom  1403  trubifal  1477  falbitruOLD  1479  exists1  2357  eqcomOLD  2430  abeq1  2545  ssequn1  3633  axpow3  4597  isocnv  6227  qextlt  11485  qextle  11486  rpnnen2  14245  odd2np1  14332  nrmmetd  21513  cusgrauvtxb  25095  cvmlift2lem12  29851  nn0prpw  30790  bj-abeq1  31166  tsbi4  32111  bicomdd  32151  ifpbicor  35851  rp-fakeoranass  35890  3impexpbicom  36504  3impexpbicomVD  36926  nabctnabc  37952
  Copyright terms: Public domain W3C validator