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  3137  raltpd  4150  opiota  6840  adderpqlem  9328  mulerpqlem  9329  lesub2  10043  rec11  10238  avglt1  10772  ixxun  11541  hashdom  12411  hashf1lem1  12466  swrdspsleq  12632  repsdf2  12709  2shfti  12872  mulre  12913  rlim  13277  rlim2  13278  nn0seqcvgd  14054  prmreclem6  14294  pwsleval  14744  issubc  15061  ismgmid  15748  grpsubeq0  15925  grpsubadd  15927  gastacos  16143  orbsta  16146  lsslss  17390  coe1mul2lem1  18079  prmirredlem  18290  prmirredlemOLD  18293  zndvds  18355  zntoslem  18362  cygznlem1  18372  islindf2  18616  restcld  19439  leordtvallem1  19477  leordtvallem2  19478  ist1-2  19614  xkoccn  19855  qtopcld  19949  ordthmeolem  20037  divstgpopn  20353  isxmet2d  20565  prdsxmetlem  20606  xblss2  20640  imasf1oxms  20727  neibl  20739  xrtgioo  21046  xrsxmet  21049  minveclem4  21582  minveclem6  21584  minveclem7  21585  mbfmulc2lem  21789  mbfmax  21791  mbfi1fseqlem4  21860  itg2gt0  21902  itg2cnlem2  21904  iblpos  21934  angrteqvd  22866  affineequiv  22885  affineequiv2  22886  dcubic  22905  rlimcnp  23023  rlimcnp2  23024  efexple  23284  bposlem7  23293  lgsabs1  23337  lgsquadlem1  23357  m1lgs  23365  colinearalg  23889  axcontlem2  23944  nb3grapr  24129  el2wlksotot  24558  rusgranumwlkl1  24623  numclwlk1lem2f1  24771  minvecolem4  25472  minvecolem6  25474  minvecolem7  25475  hvmulcan2  25666  xppreima  27159  xrge0iifcnv  27551  ballotlemsima  28094  itg2addnclem  29643  itg2addnclem2  29644  iblabsnclem  29655  areacirclem2  29685  areacirclem4  29687  dvdsabsmod0  30532  cvlcvrp  34137
  Copyright terms: Public domain W3C validator