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

Theorem 3bitr2rd 282
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
3bitr2rd  |-  ( ph  ->  ( ta  <->  ps )
)

Proof of Theorem 3bitr2rd
StepHypRef Expression
1 3bitr2d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 3bitr2d.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
31, 2bitr4d 256 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitr2d 254 1  |-  ( ph  ->  ( ta  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  fnsuppresOLD  6037  fnsuppres  6816  addsubeq4  9726  muleqadd  10081  mulle0b  10301  nn0lt10b  10807  om2uzlti  11874  qnumdenbi  13924  dprdf11  16618  dprdf11OLD  16625  lvecvscan2  17299  mplvalOLD  17609  mdetunilem9  18542  elfilss  19565  itg2seq  21336  itg2cnlem2  21356  chpchtsum  22674  bposlem7  22745  lgsdilem  22777  lgsne0  22788  axcontlem7  23351  pjnorm2  25265  cdj3lem1  25973  zrhchr  26539  dochfln0  35428  mapdindp  35622
  Copyright terms: Public domain W3C validator