ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4rd Unicode version

Theorem 3bitr4rd 210
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr4d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr4d.2  |-  ( ph  ->  ( th  <->  ps )
)
3bitr4d.3  |-  ( ph  ->  ( ta  <->  ch )
)
Assertion
Ref Expression
3bitr4rd  |-  ( ph  ->  ( ta  <->  th )
)

Proof of Theorem 3bitr4rd
StepHypRef Expression
1 3bitr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
2 3bitr4d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2bitr4d 180 . 2  |-  ( ph  ->  ( ta  <->  ps )
)
4 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
53, 4bitr4d 180 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  inimasn  4741  dmfco  5241  ltanqg  6498  genpassl  6622  genpassu  6623  ltexprlemloc  6705  caucvgprlemcanl  6742  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  caucvgprprlemaddq  6806  apneg  7602  lemuldiv  7847  msq11  7868  avglt2  8164  iooshf  8821  qtri3or  9098  sq11ap  9414  cjap  9506  sqrt11ap  9636  clim2c  9805  climabs0  9828
  Copyright terms: Public domain W3C validator