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

Theorem 3bitr2i 273
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 252 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 249 1  |-  ( ph  <->  th )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  con2bi  328  an13  799  xorneg1  1374  2eu4  2366  2eu5  2368  exists1  2374  euxfr  3271  euind  3272  rmo4  3278  2reu5lem3  3293  rmo3  3415  difin  3720  difin0ss  3880  reusv2lem4  4641  reusv6OLD  4648  reusv7OLD  4649  rabxp  5026  eliunxp  5130  imadisj  5346  intirr  5375  resco  5501  funcnv3  5639  fncnv  5642  fun11  5643  fununi  5644  f1mpt  6154  mpt2mptx  6378  uniuni  6594  frxp  6895  oeeu  7254  ixp0x  7499  mapsnen  7595  xpcomco  7609  1sdom  7724  dffi3  7893  wemapsolem  7978  cardval3  8336  kmlem4  8536  kmlem12  8544  kmlem14  8546  kmlem15  8547  kmlem16  8548  fpwwe2  9024  axgroth4  9213  ltexprlem4  9420  bitsmod  14068  pythagtrip  14340  pgpfac1  17110  pgpfac  17114  isassa  17943  istps3OLD  19401  basdif0  19432  ntreq0  19556  tgcmp  19879  tx1cn  20088  rnelfmlem  20431  phtpcer  21473  caucfil  21700  minveclem1  21817  ovoliunlem1  21891  mdegleb  22442  istrkg2ld  23836  3v3e3cycl2  24642  iswwlk  24661  adjbd1o  26982  nmo  27362  rmo3f  27372  rmo4fOLD  27373  mptfnf  27477  mpt2mptxf  27496  1stmbfm  28209  cvmlift2lem12  28737  axacprim  29057  andnand1  29840  itg2addnc  30045  asindmre  30078  fgraphopab  31146  ndmaovcom  32244  usgra2pth0  32309  eliunxp2  32791  mpt2mptx2  32792  alimp-no-surprise  33066  alsi-no-surprise  33081  onfrALTlem5  33182  bnj976  33704  bnj1143  33717  bnj1533  33778  bnj864  33848  bnj983  33877  bnj1174  33927  bnj1175  33928  bnj1280  33944  bj-denotes  34317  bj-snglc  34410  isopos  34780  dihglblem6  36942  dihglb2  36944  rp-fakeanorass  37575
  Copyright terms: Public domain W3C validator