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  2811  opiota  6290  adderpqlem  8578  mulerpqlem  8579  lesub2  9269  rec11  9458  avglt1  9949  ixxun  10672  hashdom  11361  hashf1lem1  11393  2shfti  11575  mulre  11606  rlim  11969  rlim2  11970  nn0seqcvgd  12740  prmreclem6  12968  pwsleval  13392  issubc  13712  grpsubeq0  14552  grpsubadd  14553  gastacos  14764  orbsta  14767  lsslss  15718  coe1mul2lem1  16344  prmirredlem  16446  zndvds  16503  zntoslem  16510  cygznlem1  16520  restcld  16903  leordtvallem1  16940  leordtvallem2  16941  ist1-2  17075  xkoccn  17313  qtopcld  17404  ordthmeolem  17492  divstgpopn  17802  isxmet2d  17892  prdsxmetlem  17932  xblss2  17958  imasf1oxms  18035  neibl  18047  xrtgioo  18312  xrsxmet  18315  minveclem4  18796  minveclem6  18798  minveclem7  18799  mbfmulc2lem  19002  mbfi1fseqlem4  19073  itg2gt0  19115  itg2cnlem2  19117  iblpos  19147  angrteqvd  20104  affineequiv  20123  affineequiv2  20124  dcubic  20142  rlimcnp  20260  rlimcnp2  20261  efexple  20520  bposlem7  20529  lgsabs1  20573  lgsquadlem1  20593  m1lgs  20601  minvecolem4  21459  minvecolem6  21461  minvecolem7  21462  hvmulcan2  21652  ballotlemsima  23074  xrge0iifcnv  23315  colinearalg  24538  axcontlem2  24593  areacirclem4  24927  areacirclem5  24929  grpodivzer  25377  cnfilca  25556  conttnf2  25562  dvdsabsmod0  27079  islindf2  27284  cvlcvrp  29530
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