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

Theorem 3bitr2d 281
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr2d.2  |-  ( ph  ->  ( th  <->  ch )
)
3bitr2d.3  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3bitr2d  |-  ( ph  ->  ( ps  <->  ta )
)

Proof of Theorem 3bitr2d
StepHypRef Expression
1 3bitr2d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 3bitr2d.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
31, 2bitr4d 256 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 253 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> 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:  ceqsralt  3130  raltpd  4139  opiota  6832  adderpqlem  9321  mulerpqlem  9322  lesub2  10043  rec11  10238  avglt1  10772  ixxun  11548  hashdom  12433  hashf1lem1  12491  swrdspsleq  12668  repsdf2  12744  2shfti  12998  mulre  13039  rlim  13403  rlim2  13404  nn0seqcvgd  14286  prmreclem6  14526  pwsleval  14985  issubc  15326  ismgmid  16093  grpsubeq0  16326  grpsubadd  16328  gastacos  16550  orbsta  16553  lsslss  17805  coe1mul2lem1  18506  prmirredlem  18708  zndvds  18764  zntoslem  18771  cygznlem1  18781  islindf2  19019  restcld  19843  leordtvallem1  19881  leordtvallem2  19882  ist1-2  20018  xkoccn  20289  qtopcld  20383  ordthmeolem  20471  qustgpopn  20787  isxmet2d  20999  prdsxmetlem  21040  xblss2  21074  imasf1oxms  21161  neibl  21173  xrtgioo  21480  xrsxmet  21483  minveclem4  22016  minveclem6  22018  minveclem7  22019  mbfmulc2lem  22223  mbfmax  22225  mbfi1fseqlem4  22294  itg2gt0  22336  itg2cnlem2  22338  iblpos  22368  angrteqvd  23340  affineequiv  23357  affineequiv2  23358  dcubic  23377  rlimcnp  23496  rlimcnp2  23497  efexple  23757  bposlem7  23766  lgsabs1  23810  lgsquadlem1  23830  m1lgs  23838  colinearalg  24418  axcontlem2  24473  nb3grapr  24658  el2wlksotot  25087  rusgranumwlkl1  25152  numclwlk1lem2f1  25299  minvecolem4  25997  minvecolem6  25999  minvecolem7  26000  hvmulcan2  26191  xppreima  27711  pstmxmet  28114  xrge0iifcnv  28153  ballotlemsima  28721  itg2addnclem  30309  itg2addnclem2  30310  iblabsnclem  30321  areacirclem2  30351  areacirclem4  30353  dvdsabsmod0  31170  radcnvrat  31439  logbge0b  33457  cvlcvrp  35481
  Copyright terms: Public domain W3C validator