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  6053  fnsuppres  6867  addsubeq4  9770  muleqadd  10132  mulle0b  10352  nn0lt10bOLD  10865  om2uzlti  11987  qnumdenbi  14302  dprdf11  17199  dprdf11OLD  17206  lvecvscan2  17894  mplvalOLD  18221  mdetunilem9  19230  elfilss  20485  itg2seq  22257  itg2cnlem2  22277  chpchtsum  23634  bposlem7  23705  lgsdilem  23737  lgsne0  23748  axcontlem7  24419  pjnorm2  26787  cdj3lem1  27494  zrhchr  28145  dochfln0  37656  mapdindp  37850
  Copyright terms: Public domain W3C validator