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

Theorem bicom 192
Description: Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
bicom  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )

Proof of Theorem bicom
StepHypRef Expression
1 bicom1 191 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 191 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 181 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bicomd  193  bibi1i  306  bibi1d  311  con2bi  319  ibibr  333  bibif  336  nbbn  348  pm5.17  859  biluk  900  bigolden  902  xorcom  1316  falbitru  1361  3impexpbicom  1376  mtp-xorOLD  1546  exists1  2369  eqcom  2437  abeq1  2541  ssequn1  3509  axpow3  4372  isocnv  6042  qextlt  10781  qextle  10782  rpnnen2  12817  odd2np1  12900  nrmmetd  18614  cusgrauvtxb  21497  cvmlift2lem12  24993  wl-bibi2d  26218  nn0prpw  26317  bicomdd  26680  3impexpbicomVD  28906  bnj926  29075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator