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

Theorem bitr2i 242
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 241 . 2  |-  ( ph  <->  ch )
43bicomi 194 1  |-  ( ch  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  3bitrri  264  3bitr2ri  266  3bitr4ri  270  nan  564  pm4.15  565  pm5.17  859  pm4.83  896  pm5.7  901  3or6  1265  nanim  1301  hadnot  1402  19.12vv  1921  2exsb  2208  2eu4  2363  cvjust  2430  abbi  2545  nrexralim  2744  spc3gv  3033  sbc8g  3160  ss2rab  3411  difdif  3465  ddif  3471  unass  3496  unss  3513  undi  3580  rabeq0  3641  disj  3660  ssindif0  3673  prneimg  3970  pwsnALT  4002  iinrab2  4146  unopab  4276  axrep5  4317  eqvinop  4433  pwssun  4481  pwexb  4745  suceloni  4785  dmun  5068  reldm0  5079  dmres  5159  imadmrn  5207  ssrnres  5301  dmsnn0  5327  coundi  5363  coundir  5364  cnvpo  5402  xpco  5406  fun11  5508  fununi  5509  funcnvuni  5510  isarep1  5524  dffv2  5788  fsn  5898  fconstfv  5946  eufnfv  5964  eloprabga  6152  funoprabg  6161  ralrnmpt2  6176  oprabrexex2  6181  fsplit  6443  abianfp  6708  dfer2  6898  euen1b  7170  xpsnen  7184  1sdom  7303  wemapso2lem  7511  zfregcl  7554  epfrs  7659  rankbnd  7786  rankbnd2  7787  rankxplim2  7796  rankxplim3  7797  isinfcard  7965  dfac5lem2  7997  dfac5lem5  8000  kmlem14  8035  kmlem15  8036  kmlem16  8037  axdc2lem  8320  axcclem  8329  ac9  8355  ac9s  8365  nnunb  10209  xrrebnd  10748  elfznelfzo  11184  hashfun  11692  rexuz3  12144  imasaddfnlem  13745  dprd2d2  15594  isnirred  15797  subsubrg2  15887  isdomn2  16351  tgval2  17013  0top  17040  ssntr  17114  uncmp  17458  opnfbas  17866  fbunfip  17893  hausflf2  18022  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALT  18074  metrest  18546  cfilucfil3OLD  19263  cfilucfil3  19264  ellimc3  19758  plyun0  20108  sinhalfpilem  20366  nb3graprlem2  21453  shlesb1i  22880  pjneli  23217  cnlnssadj  23575  pjin2i  23688  cvnbtwn2  23782  cvnbtwn4  23784  mdsl1i  23816  mdsl2i  23817  hatomistici  23857  cdj3lem3b  23935  iuninc  24003  disjex  24024  disjexc  24025  fdmrn  24031  isarchi2  24247  coinfliprv  24732  ballotlem2  24738  ballotlemi1  24752  dfso2  25369  dfpo2  25370  19.12b  25421  soseq  25521  dfom5b  25749  elfuns  25752  tfrqfree  25788  dfint3  25789  colinearalg  25841  axcontlem5  25899  hfext  26116  cnambfre  26245  itg2addnclem2  26247  itg2addnc  26249  trer  26310  heiborlem1  26511  ralxpxfr2d  26732  eq0rabdioph  26826  rmspecnonsq  26961  rmxdioph  27078  wopprc  27092  islssfg2  27137  2sbc6g  27583  2sbc5g  27584  iotasbc2  27588  2rexsb  27915  2rexrsb  27916  el2wlkonot  28289  el2spthonot  28290  2sb5nd  28584  2sb5ndVD  28959  2sb5ndALT  28981  bnj168  29034  bnj153  29188  bnj605  29215  bnj607  29224  bnj986  29262  bnj1090  29285  bnj1128  29296  19.12vvOLD7  29638  2exsbOLD7  29704  lssat  29751  islshpat  29752  lcvnbtwn2  29762  pclfinclN  30684  lhpex2leN  30747  diclspsn  31929  dihmeetlem4preN  32041  dihmeetlem13N  32054  lcdlss  32354  mapd1o  32383
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