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

Theorem bicom 200
Description: Commutative law for equivalence. 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 199 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 199 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 188 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
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 185
This theorem is referenced by:  bicomd  201  bibi1i  314  bibi1d  319  con2bi  328  ibibr  343  bibif  346  nbbn  358  pm5.17  886  biluk  931  bigolden  933  bianir  965  xorcom  1363  falbitru  1419  exists1  2398  eqcomOLD  2477  abeq1  2592  ssequn1  3674  axpow3  4628  isocnv  6215  qextlt  11403  qextle  11404  rpnnen2  13823  odd2np1  13908  nrmmetd  20922  cusgrauvtxb  24269  ordtconlem1  27657  cvmlift2lem12  28510  nn0prpw  29994  tsbi4  30374  bicomdd  30414  3impexpbicom  32517  3impexpbicomVD  32954  bj-abeq1  33658  frege55aid  37091
  Copyright terms: Public domain W3C validator