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  6119  fnsuppres  6924  addsubeq4  9831  muleqadd  10189  mulle0b  10409  nn0lt10b  10920  om2uzlti  12025  qnumdenbi  14132  dprdf11  16853  dprdf11OLD  16860  lvecvscan2  17541  mplvalOLD  17856  mdetunilem9  18889  elfilss  20112  itg2seq  21884  itg2cnlem2  21904  chpchtsum  23222  bposlem7  23293  lgsdilem  23325  lgsne0  23336  axcontlem7  23949  pjnorm2  26321  cdj3lem1  27029  zrhchr  27593  dochfln0  36274  mapdindp  36468
  Copyright terms: Public domain W3C validator