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

Theorem 3bitr2rd 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
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 247 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitr2d 245 1  |-  ( ph  ->  ( ta  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  fnsuppres  5748  addsubeq4  9082  muleqadd  9428  nn0lt10b  10094  om2uzlti  11029  qnumdenbi  12831  dprdf11  15274  lvecvscan2  15881  elfilss  17587  itg2seq  19113  itg2cnlem2  19133  chpchtsum  20474  bposlem7  20545  lgsdilem  20577  lgsne0  20588  pjnorm2  22322  cdj3lem1  23030  mulle0b  24102  axcontlem7  24670  dochfln0  32289  mapdindp  32483
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