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

Theorem bitr2i 241
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 240 . 2  |-  ( ph  <->  ch )
43bicomi 193 1  |-  ( ch  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  3bitrri  263  3bitr2ri  265  3bitr4ri  269  nan  563  pm4.15  564  pm5.17  858  pm4.83  895  pm5.7  900  3or6  1263  nanim  1292  hadnot  1383  19.12vv  1841  2exsb  2073  2eu4  2228  cvjust  2280  abbi  2395  spc3gv  2875  sbc8g  3000  ss2rab  3251  difdif  3304  ddif  3310  unass  3334  unss  3351  undi  3418  rabeq0  3478  disj  3497  ssindif0  3510  pwsnALT  3824  iinrab2  3967  unopab  4097  axrep5  4138  eqvinop  4253  pwssun  4301  pwundifOLD  4303  pwexb  4566  suceloni  4606  dmun  4887  reldm0  4898  dmres  4978  imadmrn  5026  ssrnres  5118  dmsnn0  5140  coundi  5176  coundir  5177  cnvpo  5215  fun11  5317  fununi  5318  funcnvuni  5319  isarep1  5333  dffv2  5594  fsn  5698  fconstfv  5736  eufnfv  5754  eloprabga  5936  funoprabg  5945  ralrnmpt2  5960  oprabrexex2  5965  fsplit  6225  abianfp  6473  dfer2  6663  euen1b  6934  xpsnen  6948  1sdom  7067  wemapso2lem  7267  zfregcl  7310  epfrs  7415  rankbnd  7542  rankbnd2  7543  rankxplim2  7552  rankxplim3  7553  isinfcard  7721  dfac5lem2  7753  dfac5lem5  7756  kmlem14  7791  kmlem15  7792  kmlem16  7793  axdc2lem  8076  axcclem  8085  ac9  8112  ac9s  8122  nnunb  9963  xrrebnd  10499  hashfun  11391  rexuz3  11834  imasaddfnlem  13432  dprd2d2  15281  isnirred  15484  subsubrg2  15574  isdomn2  16042  tgval2  16696  0top  16723  ssntr  16797  uncmp  17132  opnfbas  17539  fbunfip  17566  hausflf2  17695  alexsubALTlem2  17744  alexsubALTlem3  17745  alexsubALT  17747  metrest  18072  ellimc3  19231  plyun0  19581  sinhalfpilem  19836  shlesb1i  21967  pjneli  22304  cnlnssadj  22662  pjin2i  22775  cvnbtwn2  22869  cvnbtwn4  22871  mdsl1i  22903  mdsl2i  22904  hatomistici  22944  cdj3lem3b  23022  fdmrn  23037  ballotlem2  23049  ballotlemi1  23063  iuninc  23160  disjex  23178  disjexc  23179  coinfliprv  23685  dfso2  24113  dfpo2  24114  19.12b  24160  soseq  24256  dfom5b  24454  elfuns  24456  brimg  24478  tfrqfree  24491  colinearalg  24540  axcontlem5  24598  hfext  24815  itg2addnclem2  24934  itg2addnc  24935  negcmpprcal1  24956  eqvinopb  24976  albineal  25010  dfdir2  25302  cnvresimaOLD  26237  trer  26238  heiborlem1  26546  ralxpxfr2d  26771  eq0rabdioph  26867  rmspecnonsq  27003  rmxdioph  27120  wopprc  27134  islssfg2  27180  2sbc6g  27626  2sbc5g  27627  iotasbc2  27631  2rexsb  27959  2rexrsb  27960  prneimg  28084  2sb5nd  28382  2sb5ndVD  28759  2sb5ndALT  28782  bnj168  28831  bnj153  28985  bnj605  29012  bnj607  29021  bnj986  29059  bnj1090  29082  bnj1128  29093  equvinv  29187  a12study4  29190  a12study9  29193  a12peros  29194  lssat  29279  islshpat  29280  lcvnbtwn2  29290  pclfinclN  30212  lhpex2leN  30275  diclspsn  31457  dihmeetlem4preN  31569  dihmeetlem13N  31582  lcdlss  31882  mapd1o  31911
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