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

Theorem 3bitr2rd 274
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 248 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitr2d 246 1  |-  ( ph  ->  ( ta  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  fnsuppres  5892  addsubeq4  9253  muleqadd  9599  nn0lt10b  10269  om2uzlti  11218  qnumdenbi  13064  dprdf11  15509  lvecvscan2  16112  elfilss  17830  itg2seq  19502  itg2cnlem2  19522  chpchtsum  20871  bposlem7  20942  lgsdilem  20974  lgsne0  20985  pjnorm2  23078  cdj3lem1  23786  zrhchr  24160  mulle0b  24972  axcontlem7  25624  dochfln0  31593  mapdindp  31787
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