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

Theorem bicom 191
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 190 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 190 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 180 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bicomd  192  bibi1i  305  bibi1d  310  con2bi  318  ibibr  332  bibif  335  nbbn  347  pm5.17  858  biluk  899  bigolden  901  xorcom  1307  falbitru  1352  3impexpbicom  1367  mtp-xorOLD  1537  exists1  2298  eqcom  2360  abeq1  2464  ssequn1  3421  axpow3  4272  isocnv  5914  qextlt  10622  qextle  10623  rpnnen2  12601  odd2np1  12684  nrmmetd  18199  bisimpd  23141  iuninc  23210  cvmlift2lem12  24249  wl-bibi2d  25475  nn0prpw  25563  bicomdd  26028  compneOLD  26966  aibandbiaiffaiffb  27185  aibandbiaiaiffb  27186  notatnand  27187  aistia  27188  aisfina  27189  bothfbothsame  27191  aiffnbandciffatnotciffb  27195  axorbciffatcxorb  27196  aibnbna  27197  aisbnaxb  27202  abnotbtaxb  27207  abnotataxb  27208  cusgrauvtxb  27659  3impexpbicomVD  28395  bnj926  28561
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 177
  Copyright terms: Public domain W3C validator