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  1839  2exsb  2071  2eu4  2226  cvjust  2278  abbi  2393  spc3gv  2873  sbc8g  2998  ss2rab  3249  difdif  3302  ddif  3308  unass  3332  unss  3349  undi  3416  rabeq0  3476  disj  3495  ssindif0  3508  pwsnALT  3822  iinrab2  3965  unopab  4095  axrep5  4136  eqvinop  4251  pwssun  4299  pwundifOLD  4301  pwexb  4564  suceloni  4604  dmun  4885  reldm0  4896  dmres  4976  imadmrn  5024  ssrnres  5116  dmsnn0  5138  coundi  5174  coundir  5175  cnvpo  5213  fun11  5315  fununi  5316  funcnvuni  5317  isarep1  5331  dffv2  5592  fsn  5696  fconstfv  5734  eufnfv  5752  eloprabga  5934  funoprabg  5943  ralrnmpt2  5958  oprabrexex2  5963  fsplit  6223  abianfp  6471  dfer2  6661  euen1b  6932  xpsnen  6946  1sdom  7065  wemapso2lem  7265  zfregcl  7308  epfrs  7413  rankbnd  7540  rankbnd2  7541  rankxplim2  7550  rankxplim3  7551  isinfcard  7719  dfac5lem2  7751  dfac5lem5  7754  kmlem14  7789  kmlem15  7790  kmlem16  7791  axdc2lem  8074  axcclem  8083  ac9  8110  ac9s  8120  nnunb  9961  xrrebnd  10497  hashfun  11389  rexuz3  11832  imasaddfnlem  13430  dprd2d2  15279  isnirred  15482  subsubrg2  15572  isdomn2  16040  tgval2  16694  0top  16721  ssntr  16795  uncmp  17130  opnfbas  17537  fbunfip  17564  hausflf2  17693  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALT  17745  metrest  18070  ellimc3  19229  plyun0  19579  sinhalfpilem  19834  shlesb1i  21965  pjneli  22302  cnlnssadj  22660  pjin2i  22773  cvnbtwn2  22867  cvnbtwn4  22869  mdsl1i  22901  mdsl2i  22902  hatomistici  22942  cdj3lem3b  23020  fdmrn  23035  ballotlem2  23047  ballotlemi1  23061  iuninc  23158  disjex  23176  disjexc  23177  coinfliprv  23683  dfso2  24111  dfpo2  24112  19.12b  24158  soseq  24254  dfom5b  24452  elfuns  24454  brimg  24476  tfrqfree  24489  colinearalg  24538  axcontlem5  24596  hfext  24813  negcmpprcal1  24945  eqvinopb  24965  albineal  24999  dfdir2  25291  cnvresimaOLD  26226  trer  26227  heiborlem1  26535  ralxpxfr2d  26760  eq0rabdioph  26856  rmspecnonsq  26992  rmxdioph  27109  wopprc  27123  islssfg2  27169  2sbc6g  27615  2sbc5g  27616  iotasbc2  27620  2rexsb  27948  2rexrsb  27949  prneimg  28073  2sb5nd  28326  2sb5ndVD  28686  2sb5ndALT  28709  bnj168  28758  bnj153  28912  bnj605  28939  bnj607  28948  bnj986  28986  bnj1090  29009  bnj1128  29020  equvinv  29114  a12study4  29117  a12study9  29120  a12peros  29121  lssat  29206  islshpat  29207  lcvnbtwn2  29217  pclfinclN  30139  lhpex2leN  30202  diclspsn  31384  dihmeetlem4preN  31496  dihmeetlem13N  31509  lcdlss  31809  mapd1o  31838
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