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

Theorem bicom 204
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 203 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 203 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 191 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188
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 189
This theorem is referenced by:  bicomd  205  bibi1i  316  bibi1d  321  con2bi  330  ibibr  345  bibif  348  nbbn  360  pm5.17  898  biluk  943  bigolden  945  bianirOLD  978  xorcom  1407  trubifal  1481  falbitruOLD  1483  exists1  2389  abeq1  2560  ssequn1  3603  axpow3  4583  isocnv  6219  qextlt  11493  qextle  11494  rpnnen2  14271  odd2np1  14358  nrmmetd  21582  cusgrauvtxb  25217  cvmlift2lem12  30030  nn0prpw  30972  bj-abeq1  31382  tsbi4  32371  bicomdd  32411  ifpbicor  36113  rp-fakeoranass  36152  3impexpbicom  36828  3impexpbicomVD  37247  nabctnabc  38513
  Copyright terms: Public domain W3C validator