MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr2d 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  2939  opiota  6494  adderpqlem  8787  mulerpqlem  8788  lesub2  9479  rec11  9668  avglt1  10161  ixxun  10888  hashdom  11608  hashf1lem1  11659  2shfti  11850  mulre  11881  rlim  12244  rlim2  12245  nn0seqcvgd  13016  prmreclem6  13244  pwsleval  13670  issubc  13990  ismgmid  14665  grpsubeq0  14830  grpsubadd  14831  gastacos  15042  orbsta  15045  lsslss  15992  coe1mul2lem1  16615  prmirredlem  16728  zndvds  16785  zntoslem  16792  cygznlem1  16802  restcld  17190  leordtvallem1  17228  leordtvallem2  17229  ist1-2  17365  xkoccn  17604  qtopcld  17698  ordthmeolem  17786  divstgpopn  18102  isxmet2d  18310  prdsxmetlem  18351  xblss2  18385  imasf1oxms  18472  neibl  18484  xrtgioo  18790  xrsxmet  18793  minveclem4  19286  minveclem6  19288  minveclem7  19289  mbfmulc2lem  19492  mbfmax  19494  mbfi1fseqlem4  19563  itg2gt0  19605  itg2cnlem2  19607  iblpos  19637  angrteqvd  20601  affineequiv  20620  affineequiv2  20621  dcubic  20639  rlimcnp  20757  rlimcnp2  20758  efexple  21018  bposlem7  21027  lgsabs1  21071  lgsquadlem1  21091  m1lgs  21099  nb3grapr  21415  minvecolem4  22335  minvecolem6  22337  minvecolem7  22338  hvmulcan2  22528  xppreima  24012  xrge0iifcnv  24272  ballotlemsima  24726  colinearalg  25753  axcontlem2  25808  itg2addnclem  26155  itg2addnclem2  26156  iblabsnclem  26167  areacirclem4  26183  areacirclem5  26185  dvdsabsmod0  26947  islindf2  27152  el2wlksotot  28079  cvlcvrp  29823
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