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

Theorem bitr2i 243
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr2i.1  |-  ( ph  <->  ps )
bitr2i.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
bitr2i  |-  ( ch  <->  ph )

Proof of Theorem bitr2i
StepHypRef Expression
1 bitr2i.1 . . 3  |-  ( ph  <->  ps )
2 bitr2i.2 . . 3  |-  ( ps  <->  ch )
31, 2bitri 242 . 2  |-  ( ph  <->  ch )
43bicomi 195 1  |-  ( ch  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  3bitrri  265  3bitr2ri  267  3bitr4ri  271  nan  565  pm4.15  566  pm5.17  860  pm4.83  897  pm5.7  902  3or6  1266  nanim  1302  hadnot  1403  19.12vv  1922  2exsb  2211  2eu4  2366  cvjust  2433  abbi  2548  nrexralim  2754  spc3gv  3043  sbc8g  3170  ss2rab  3421  difdif  3475  ddif  3481  unass  3506  unss  3523  undi  3590  rabeq0  3651  disj  3670  ssindif0  3683  prneimg  3980  pwsnALT  4012  iinrab2  4156  unopab  4286  axrep5  4327  eqvinop  4443  pwssun  4491  pwexb  4755  suceloni  4795  dmun  5078  reldm0  5089  dmres  5169  imadmrn  5217  ssrnres  5311  dmsnn0  5337  coundi  5373  coundir  5374  cnvpo  5412  xpco  5416  fun11  5518  fununi  5519  funcnvuni  5520  isarep1  5534  dffv2  5798  fsn  5908  fconstfv  5956  eufnfv  5974  eloprabga  6162  funoprabg  6171  ralrnmpt2  6186  oprabrexex2  6191  fsplit  6453  abianfp  6718  dfer2  6908  euen1b  7180  xpsnen  7194  1sdom  7313  wemapso2lem  7521  zfregcl  7564  epfrs  7669  rankbnd  7796  rankbnd2  7797  rankxplim2  7806  rankxplim3  7807  isinfcard  7975  dfac5lem2  8007  dfac5lem5  8010  kmlem14  8045  kmlem15  8046  kmlem16  8047  axdc2lem  8330  axcclem  8339  ac9  8365  ac9s  8375  nnunb  10219  xrrebnd  10758  elfznelfzo  11194  hashfun  11702  rexuz3  12154  imasaddfnlem  13755  dprd2d2  15604  isnirred  15807  subsubrg2  15897  isdomn2  16361  tgval2  17023  0top  17050  ssntr  17124  uncmp  17468  opnfbas  17876  fbunfip  17903  hausflf2  18032  alexsubALTlem2  18081  alexsubALTlem3  18082  alexsubALT  18084  metrest  18556  cfilucfil3OLD  19273  cfilucfil3  19274  ellimc3  19768  plyun0  20118  sinhalfpilem  20376  nb3graprlem2  21463  shlesb1i  22890  pjneli  23227  cnlnssadj  23585  pjin2i  23698  cvnbtwn2  23792  cvnbtwn4  23794  mdsl1i  23826  mdsl2i  23827  hatomistici  23867  cdj3lem3b  23945  iuninc  24013  disjex  24034  disjexc  24035  fdmrn  24041  isarchi2  24257  coinfliprv  24742  ballotlem2  24748  ballotlemi1  24762  dfso2  25379  dfpo2  25380  19.12b  25431  soseq  25531  dfom5b  25759  elfuns  25762  tfrqfree  25798  dfint3  25799  colinearalg  25851  axcontlem5  25909  hfext  26126  cnambfre  26257  itg2addnclem2  26259  itg2addnc  26261  trer  26321  heiborlem1  26522  ralxpxfr2d  26743  eq0rabdioph  26837  rmspecnonsq  26972  rmxdioph  27089  wopprc  27103  islssfg2  27148  2sbc6g  27594  2sbc5g  27595  iotasbc2  27599  2rexsb  27926  2rexrsb  27927  2wlkeq  28329  el2wlkonot  28389  el2spthonot  28390  2sb5nd  28709  2sb5ndVD  29084  2sb5ndALT  29106  bnj168  29159  bnj153  29313  bnj605  29340  bnj607  29349  bnj986  29387  bnj1090  29410  bnj1128  29421  19.12vvOLD7  29763  2exsbOLD7  29829  lssat  29876  islshpat  29877  lcvnbtwn2  29887  pclfinclN  30809  lhpex2leN  30872  diclspsn  32054  dihmeetlem4preN  32166  dihmeetlem13N  32179  lcdlss  32479  mapd1o  32508
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 179
  Copyright terms: Public domain W3C validator