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  1910  2exsb  2166  2eu4  2321  cvjust  2382  abbi  2497  spc3gv  2984  sbc8g  3111  ss2rab  3362  difdif  3416  ddif  3422  unass  3447  unss  3464  undi  3531  rabeq0  3592  disj  3611  ssindif0  3624  prneimg  3920  pwsnALT  3952  iinrab2  4095  unopab  4225  axrep5  4266  eqvinop  4382  pwssun  4430  pwexb  4693  suceloni  4733  dmun  5016  reldm0  5027  dmres  5107  imadmrn  5155  ssrnres  5249  dmsnn0  5275  coundi  5311  coundir  5312  cnvpo  5350  xpco  5354  fun11  5456  fununi  5457  funcnvuni  5458  isarep1  5472  dffv2  5735  fsn  5845  fconstfv  5893  eufnfv  5911  eloprabga  6099  funoprabg  6108  ralrnmpt2  6123  oprabrexex2  6128  fsplit  6390  abianfp  6652  dfer2  6842  euen1b  7114  xpsnen  7128  1sdom  7247  wemapso2lem  7452  zfregcl  7495  epfrs  7600  rankbnd  7727  rankbnd2  7728  rankxplim2  7737  rankxplim3  7738  isinfcard  7906  dfac5lem2  7938  dfac5lem5  7941  kmlem14  7976  kmlem15  7977  kmlem16  7978  axdc2lem  8261  axcclem  8270  ac9  8296  ac9s  8306  nnunb  10149  xrrebnd  10688  elfznelfzo  11119  hashfun  11627  rexuz3  12079  imasaddfnlem  13680  dprd2d2  15529  isnirred  15732  subsubrg2  15822  isdomn2  16286  tgval2  16944  0top  16971  ssntr  17045  uncmp  17388  opnfbas  17795  fbunfip  17822  hausflf2  17951  alexsubALTlem2  18000  alexsubALTlem3  18001  alexsubALT  18003  metrest  18444  cfilucfil3  19142  ellimc3  19633  plyun0  19983  sinhalfpilem  20241  nb3graprlem2  21327  shlesb1i  22736  pjneli  23073  cnlnssadj  23431  pjin2i  23544  cvnbtwn2  23638  cvnbtwn4  23640  mdsl1i  23672  mdsl2i  23673  hatomistici  23713  cdj3lem3b  23791  iuninc  23855  disjex  23875  disjexc  23876  fdmrn  23882  coinfliprv  24519  ballotlem2  24525  ballotlemi1  24539  dfso2  25135  dfpo2  25136  19.12b  25182  soseq  25278  dfom5b  25476  elfuns  25478  brimg  25500  tfrqfree  25514  colinearalg  25563  axcontlem5  25621  hfext  25838  itg2addnclem2  25958  itg2addnc  25959  trer  26010  heiborlem1  26211  ralxpxfr2d  26432  eq0rabdioph  26526  rmspecnonsq  26661  rmxdioph  26778  wopprc  26792  islssfg2  26838  2sbc6g  27284  2sbc5g  27285  iotasbc2  27289  2rexsb  27616  2rexrsb  27617  2sb5nd  27990  2sb5ndVD  28363  2sb5ndALT  28386  bnj168  28435  bnj153  28589  bnj605  28616  bnj607  28625  bnj986  28663  bnj1090  28686  bnj1128  28697  19.12vvOLD7  29017  2exsbOLD7  29084  lssat  29131  islshpat  29132  lcvnbtwn2  29142  pclfinclN  30064  lhpex2leN  30127  diclspsn  31309  dihmeetlem4preN  31421  dihmeetlem13N  31434  lcdlss  31734  mapd1o  31763
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