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

Theorem 3bitr2i 266
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1  |-  ( ph  <->  ps )
3bitr2i.2  |-  ( ch  <->  ps )
3bitr2i.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitr2i  |-  ( ph  <->  th )

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3  |-  ( ph  <->  ps )
2 3bitr2i.2 . . 3  |-  ( ch  <->  ps )
31, 2bitr4i 245 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 242 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  con2bi  320  an13  777  xorneg1  1307  2eu5  2197  exists1  2202  euxfr  2888  rmo4  2897  rmo3  3006  difin  3313  difin0ss  3426  uniuni  4418  reusv2lem4  4429  reusv6OLD  4436  reusv7OLD  4437  rabxp  4632  eliunxp  4730  imadisj  4939  intirr  4968  resco  5083  funcnv3  5168  fncnv  5171  fun11  5172  fununi  5173  mpt2mptx  5790  frxp  6077  oeeu  6487  ixp0x  6730  mapsnen  6823  xpcomco  6837  1sdom  6950  dffi3  7068  cardval3  7469  kmlem4  7663  kmlem12  7671  kmlem14  7673  kmlem15  7674  kmlem16  7675  fpwwe2  8145  axgroth4  8334  ltexprlem4  8543  bitsmod  12501  pythagtrip  12761  pgpfac1  15150  pgpfac  15154  isassa  15888  istps3OLD  16492  basdif0  16523  ntreq0  16646  tgcmp  16960  tx1cn  17135  rnelfmlem  17479  phtpcer  18325  caucfil  18541  minveclem1  18620  ovoliunlem1  18693  mdegleb  19282  adjbd1o  22495  cvmlift2lem12  23016  axacprim  23224  axfelem18  23531  brimg  23650  andnand1  24011  and4com  24105  fgraphopab  26695  onfrALTlem5  27000  bnj976  27498  bnj1143  27511  bnj1533  27573  bnj864  27643  bnj983  27672  bnj1174  27722  bnj1175  27723  bnj1280  27739  isopos  28059  dihglblem6  30219  dihglb2  30221
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator