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

Theorem 3bitr2i 264
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 243 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 240 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  con2bi  318  an13  774  xorneg1  1302  2eu5  2240  exists1  2245  euxfr  2964  rmo4  2971  2reu5lem3  2985  rmo3  3091  difin  3419  difin0ss  3533  uniuni  4543  reusv2lem4  4554  reusv6OLD  4561  reusv7OLD  4562  rabxp  4741  eliunxp  4839  imadisj  5048  intirr  5077  resco  5193  funcnv3  5327  fncnv  5330  fun11  5331  fununi  5332  mpt2mptx  5954  frxp  6241  oeeu  6617  ixp0x  6860  mapsnen  6954  xpcomco  6968  1sdom  7081  dffi3  7200  cardval3  7601  kmlem4  7795  kmlem12  7803  kmlem14  7805  kmlem15  7806  kmlem16  7807  fpwwe2  8281  axgroth4  8470  ltexprlem4  8679  bitsmod  12643  pythagtrip  12903  pgpfac1  15331  pgpfac  15335  isassa  16072  istps3OLD  16676  basdif0  16707  ntreq0  16830  tgcmp  17144  tx1cn  17319  rnelfmlem  17663  phtpcer  18509  caucfil  18725  minveclem1  18804  ovoliunlem1  18877  mdegleb  19466  adjbd1o  22681  nmo  23160  rmo3f  23194  rmo4fOLD  23195  mptfnf  23241  1stmbfm  23580  cvmlift2lem12  23860  axacprim  24068  brimg  24547  andnand1  24909  itg2addnc  25005  and4com  25043  fgraphopab  27632  ndmaovcom  28173  3v3e3cycl2  28410  onfrALTlem5  28606  bnj976  29125  bnj1143  29138  bnj1533  29200  bnj864  29270  bnj983  29299  bnj1174  29349  bnj1175  29350  bnj1280  29366  isopos  29992  dihglblem6  32152  dihglb2  32154
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