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  3001  raltpd  4003  opiota  6638  adderpqlem  9128  mulerpqlem  9129  lesub2  9839  rec11  10034  avglt1  10567  ixxun  11321  hashdom  12147  hashf1lem1  12213  swrdspsleq  12347  repsdf2  12421  2shfti  12574  mulre  12615  rlim  12978  rlim2  12979  nn0seqcvgd  13750  prmreclem6  13987  pwsleval  14436  issubc  14753  ismgmid  15440  grpsubeq0  15617  grpsubadd  15618  gastacos  15833  orbsta  15836  lsslss  17047  coe1mul2lem1  17726  prmirredlem  17922  prmirredlemOLD  17925  zndvds  17987  zntoslem  17994  cygznlem1  18004  islindf2  18248  restcld  18781  leordtvallem1  18819  leordtvallem2  18820  ist1-2  18956  xkoccn  19197  qtopcld  19291  ordthmeolem  19379  divstgpopn  19695  isxmet2d  19907  prdsxmetlem  19948  xblss2  19982  imasf1oxms  20069  neibl  20081  xrtgioo  20388  xrsxmet  20391  minveclem4  20924  minveclem6  20926  minveclem7  20927  mbfmulc2lem  21130  mbfmax  21132  mbfi1fseqlem4  21201  itg2gt0  21243  itg2cnlem2  21245  iblpos  21275  angrteqvd  22207  affineequiv  22226  affineequiv2  22227  dcubic  22246  rlimcnp  22364  rlimcnp2  22365  efexple  22625  bposlem7  22634  lgsabs1  22678  lgsquadlem1  22698  m1lgs  22706  colinearalg  23161  axcontlem2  23216  nb3grapr  23366  minvecolem4  24286  minvecolem6  24288  minvecolem7  24289  hvmulcan2  24480  xppreima  25969  xrge0iifcnv  26368  ballotlemsima  26903  itg2addnclem  28448  itg2addnclem2  28449  iblabsnclem  28460  areacirclem2  28490  areacirclem4  28492  dvdsabsmod0  29340  el2wlksotot  30406  rusgranumwlkl1  30564  numclwlk1lem2f1  30692  cvlcvrp  32990
  Copyright terms: Public domain W3C validator