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

Theorem 3bitr2d 284
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 259 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 256 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  ceqsralt  3047  raltpd  4066  opiota  6810  adderpqlem  9330  mulerpqlem  9331  lesub2  10060  rec11  10256  avglt1  10801  ixxun  11602  hashdom  12508  hashf1lem1  12566  swrdspsleq  12751  repsdf2  12827  2shfti  13087  mulre  13128  rlim  13502  rlim2  13503  nn0seqcvgd  14472  prmreclem6  14808  pwsleval  15334  issubc  15683  ismgmid  16450  grpsubeq0  16683  grpsubadd  16685  gastacos  16907  orbsta  16910  lsslss  18127  coe1mul2lem1  18803  prmirredlem  19006  zndvds  19062  zntoslem  19069  cygznlem1  19079  islindf2  19314  restcld  20130  leordtvallem1  20168  leordtvallem2  20169  ist1-2  20305  xkoccn  20576  qtopcld  20670  ordthmeolem  20758  qustgpopn  21076  isxmet2d  21284  prdsxmetlem  21325  xblss2  21359  imasf1oxms  21446  neibl  21458  xrtgioo  21766  xrsxmet  21769  minveclem4  22316  minveclem6  22318  minveclem7  22319  minveclem4OLD  22328  minveclem6OLD  22330  minveclem7OLD  22331  mbfmulc2lem  22545  mbfmax  22547  mbfi1fseqlem4  22618  itg2gt0  22660  itg2cnlem2  22662  iblpos  22692  angrteqvd  23677  affineequiv  23694  affineequiv2  23695  dcubic  23714  rlimcnp  23833  rlimcnp2  23834  efexple  24151  bposlem7  24160  lgsabs1  24204  lgsquadlem1  24224  m1lgs  24232  lnhl  24602  colinearalg  24882  axcontlem2  24937  nb3grapr  25123  el2wlksotot  25552  rusgranumwlkl1  25617  numclwlk1lem2f1  25764  minvecolem4  26464  minvecolem6  26466  minvecolem7  26467  minvecolem4OLD  26474  minvecolem6OLD  26476  minvecolem7OLD  26477  hvmulcan2  26668  xppreima  28194  smatrcl  28574  pstmxmet  28652  xrge0iifcnv  28691  ballotlemsima  29300  ballotlemsimaOLD  29338  poimirlem27  31874  itg2addnclem  31900  itg2addnclem2  31901  iblabsnclem  31912  areacirclem2  31940  areacirclem4  31942  cvlcvrp  32818  dvdsabsmod0OLD  35754  radcnvrat  36576  nbupgrel  39159  nb3grpr  39197  logbge0b  39977
  Copyright terms: Public domain W3C validator