MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr2i 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  1298  hadnot  1399  19.12vv  1917  2exsb  2182  2eu4  2337  cvjust  2399  abbi  2514  spc3gv  3001  sbc8g  3128  ss2rab  3379  difdif  3433  ddif  3439  unass  3464  unss  3481  undi  3548  rabeq0  3609  disj  3628  ssindif0  3641  prneimg  3938  pwsnALT  3970  iinrab2  4114  unopab  4244  axrep5  4285  eqvinop  4401  pwssun  4449  pwexb  4712  suceloni  4752  dmun  5035  reldm0  5046  dmres  5126  imadmrn  5174  ssrnres  5268  dmsnn0  5294  coundi  5330  coundir  5331  cnvpo  5369  xpco  5373  fun11  5475  fununi  5476  funcnvuni  5477  isarep1  5491  dffv2  5755  fsn  5865  fconstfv  5913  eufnfv  5931  eloprabga  6119  funoprabg  6128  ralrnmpt2  6143  oprabrexex2  6148  fsplit  6410  abianfp  6675  dfer2  6865  euen1b  7137  xpsnen  7151  1sdom  7270  wemapso2lem  7475  zfregcl  7518  epfrs  7623  rankbnd  7750  rankbnd2  7751  rankxplim2  7760  rankxplim3  7761  isinfcard  7929  dfac5lem2  7961  dfac5lem5  7964  kmlem14  7999  kmlem15  8000  kmlem16  8001  axdc2lem  8284  axcclem  8293  ac9  8319  ac9s  8329  nnunb  10173  xrrebnd  10712  elfznelfzo  11147  hashfun  11655  rexuz3  12107  imasaddfnlem  13708  dprd2d2  15557  isnirred  15760  subsubrg2  15850  isdomn2  16314  tgval2  16976  0top  17003  ssntr  17077  uncmp  17420  opnfbas  17827  fbunfip  17854  hausflf2  17983  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALT  18035  metrest  18507  cfilucfil3OLD  19224  cfilucfil3  19225  ellimc3  19719  plyun0  20069  sinhalfpilem  20327  nb3graprlem2  21414  shlesb1i  22841  pjneli  23178  cnlnssadj  23536  pjin2i  23649  cvnbtwn2  23743  cvnbtwn4  23745  mdsl1i  23777  mdsl2i  23778  hatomistici  23818  cdj3lem3b  23896  iuninc  23964  disjex  23985  disjexc  23986  fdmrn  23992  isarchi2  24208  coinfliprv  24693  ballotlem2  24699  ballotlemi1  24713  dfso2  25325  dfpo2  25326  19.12b  25372  soseq  25468  dfom5b  25666  elfuns  25668  brimg  25690  tfrqfree  25704  colinearalg  25753  axcontlem5  25811  hfext  26028  cnambfre  26154  itg2addnclem2  26156  itg2addnc  26158  trer  26209  heiborlem1  26410  ralxpxfr2d  26631  eq0rabdioph  26725  rmspecnonsq  26860  rmxdioph  26977  wopprc  26991  islssfg2  27037  2sbc6g  27483  2sbc5g  27484  iotasbc2  27488  2rexsb  27815  2rexrsb  27816  el2wlkonot  28066  el2spthonot  28067  2sb5nd  28358  2sb5ndVD  28731  2sb5ndALT  28754  bnj168  28803  bnj153  28957  bnj605  28984  bnj607  28993  bnj986  29031  bnj1090  29054  bnj1128  29065  19.12vvOLD7  29385  2exsbOLD7  29452  lssat  29499  islshpat  29500  lcvnbtwn2  29510  pclfinclN  30432  lhpex2leN  30495  diclspsn  31677  dihmeetlem4preN  31789  dihmeetlem13N  31802  lcdlss  32102  mapd1o  32131
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