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

Theorem 3bitr2d 273
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 248 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 245 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  ceqsralt  2979  opiota  6535  adderpqlem  8831  mulerpqlem  8832  lesub2  9523  rec11  9712  avglt1  10205  ixxun  10932  hashdom  11653  hashf1lem1  11704  2shfti  11895  mulre  11926  rlim  12289  rlim2  12290  nn0seqcvgd  13061  prmreclem6  13289  pwsleval  13715  issubc  14035  ismgmid  14710  grpsubeq0  14875  grpsubadd  14876  gastacos  15087  orbsta  15090  lsslss  16037  coe1mul2lem1  16660  prmirredlem  16773  zndvds  16830  zntoslem  16837  cygznlem1  16847  restcld  17236  leordtvallem1  17274  leordtvallem2  17275  ist1-2  17411  xkoccn  17651  qtopcld  17745  ordthmeolem  17833  divstgpopn  18149  isxmet2d  18357  prdsxmetlem  18398  xblss2  18432  imasf1oxms  18519  neibl  18531  xrtgioo  18837  xrsxmet  18840  minveclem4  19333  minveclem6  19335  minveclem7  19336  mbfmulc2lem  19539  mbfmax  19541  mbfi1fseqlem4  19610  itg2gt0  19652  itg2cnlem2  19654  iblpos  19684  angrteqvd  20648  affineequiv  20667  affineequiv2  20668  dcubic  20686  rlimcnp  20804  rlimcnp2  20805  efexple  21065  bposlem7  21074  lgsabs1  21118  lgsquadlem1  21138  m1lgs  21146  nb3grapr  21462  minvecolem4  22382  minvecolem6  22384  minvecolem7  22385  hvmulcan2  22575  xppreima  24059  xrge0iifcnv  24319  ballotlemsima  24773  colinearalg  25849  axcontlem2  25904  itg2addnclem  26256  itg2addnclem2  26257  iblabsnclem  26268  areacirclem2  26293  areacirclem4  26295  dvdsabsmod0  27057  islindf2  27261  el2wlksotot  28349  cvlcvrp  30138
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator