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  1851  2exsb  2084  2eu4  2239  cvjust  2291  abbi  2406  spc3gv  2886  sbc8g  3011  ss2rab  3262  difdif  3315  ddif  3321  unass  3345  unss  3362  undi  3429  rabeq0  3489  disj  3508  ssindif0  3521  pwsnALT  3838  iinrab2  3981  unopab  4111  axrep5  4152  eqvinop  4267  pwssun  4315  pwundifOLD  4317  pwexb  4580  suceloni  4620  dmun  4901  reldm0  4912  dmres  4992  imadmrn  5040  ssrnres  5132  dmsnn0  5154  coundi  5190  coundir  5191  cnvpo  5229  fun11  5331  fununi  5332  funcnvuni  5333  isarep1  5347  dffv2  5608  fsn  5712  fconstfv  5750  eufnfv  5768  eloprabga  5950  funoprabg  5959  ralrnmpt2  5974  oprabrexex2  5979  fsplit  6239  abianfp  6487  dfer2  6677  euen1b  6948  xpsnen  6962  1sdom  7081  wemapso2lem  7281  zfregcl  7324  epfrs  7429  rankbnd  7556  rankbnd2  7557  rankxplim2  7566  rankxplim3  7567  isinfcard  7735  dfac5lem2  7767  dfac5lem5  7770  kmlem14  7805  kmlem15  7806  kmlem16  7807  axdc2lem  8090  axcclem  8099  ac9  8126  ac9s  8136  nnunb  9977  xrrebnd  10513  hashfun  11405  rexuz3  11848  imasaddfnlem  13446  dprd2d2  15295  isnirred  15498  subsubrg2  15588  isdomn2  16056  tgval2  16710  0top  16737  ssntr  16811  uncmp  17146  opnfbas  17553  fbunfip  17580  hausflf2  17709  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALT  17761  metrest  18086  ellimc3  19245  plyun0  19595  sinhalfpilem  19850  shlesb1i  21981  pjneli  22318  cnlnssadj  22676  pjin2i  22789  cvnbtwn2  22883  cvnbtwn4  22885  mdsl1i  22917  mdsl2i  22918  hatomistici  22958  cdj3lem3b  23036  fdmrn  23051  ballotlem2  23063  ballotlemi1  23077  iuninc  23174  disjex  23192  disjexc  23193  coinfliprv  23698  dfso2  24182  dfpo2  24183  19.12b  24229  soseq  24325  dfom5b  24523  elfuns  24525  brimg  24547  tfrqfree  24561  colinearalg  24610  axcontlem5  24668  hfext  24885  itg2addnclem2  25004  itg2addnc  25005  negcmpprcal1  25048  eqvinopb  25068  albineal  25102  dfdir2  25394  cnvresimaOLD  26329  trer  26330  heiborlem1  26638  ralxpxfr2d  26863  eq0rabdioph  26959  rmspecnonsq  27095  rmxdioph  27212  wopprc  27226  islssfg2  27272  2sbc6g  27718  2sbc5g  27719  iotasbc2  27723  2rexsb  28051  2rexrsb  28052  prneimg  28183  elfznelfzo  28213  nb3graprlem2  28288  2sb5nd  28625  2sb5ndVD  29002  2sb5ndALT  29025  bnj168  29074  bnj153  29228  bnj605  29255  bnj607  29264  bnj986  29302  bnj1090  29325  bnj1128  29336  19.12vvOLD7  29655  2exsbOLD7  29723  equvinv  29736  a12study4  29739  a12study9  29742  a12peros  29743  lssat  29828  islshpat  29829  lcvnbtwn2  29839  pclfinclN  30761  lhpex2leN  30824  diclspsn  32006  dihmeetlem4preN  32118  dihmeetlem13N  32131  lcdlss  32431  mapd1o  32460
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