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

Theorem 3bitr2d 272
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 247 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 244 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ceqsralt  2824  opiota  6306  adderpqlem  8594  mulerpqlem  8595  lesub2  9285  rec11  9474  avglt1  9965  ixxun  10688  hashdom  11377  hashf1lem1  11409  2shfti  11591  mulre  11622  rlim  11985  rlim2  11986  nn0seqcvgd  12756  prmreclem6  12984  pwsleval  13408  issubc  13728  grpsubeq0  14568  grpsubadd  14569  gastacos  14780  orbsta  14783  lsslss  15734  coe1mul2lem1  16360  prmirredlem  16462  zndvds  16519  zntoslem  16526  cygznlem1  16536  restcld  16919  leordtvallem1  16956  leordtvallem2  16957  ist1-2  17091  xkoccn  17329  qtopcld  17420  ordthmeolem  17508  divstgpopn  17818  isxmet2d  17908  prdsxmetlem  17948  xblss2  17974  imasf1oxms  18051  neibl  18063  xrtgioo  18328  xrsxmet  18331  minveclem4  18812  minveclem6  18814  minveclem7  18815  mbfmulc2lem  19018  mbfi1fseqlem4  19089  itg2gt0  19131  itg2cnlem2  19133  iblpos  19163  angrteqvd  20120  affineequiv  20139  affineequiv2  20140  dcubic  20158  rlimcnp  20276  rlimcnp2  20277  efexple  20536  bposlem7  20545  lgsabs1  20589  lgsquadlem1  20609  m1lgs  20617  minvecolem4  21475  minvecolem6  21477  minvecolem7  21478  hvmulcan2  21668  ballotlemsima  23090  xrge0iifcnv  23330  colinearalg  24610  axcontlem2  24665  itg2addnclem  25003  itg2addnclem2  25004  itgaddnclem2  25010  iblabsnclem  25014  areacirclem4  25030  areacirclem5  25032  grpodivzer  25480  cnfilca  25659  conttnf2  25665  dvdsabsmod0  27182  islindf2  27387  nb3grapr  28289  cvlcvrp  30152
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 177
  Copyright terms: Public domain W3C validator