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

Theorem 3bitr4rd 219
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 189 . 2  |-  ( ph  ->  ( ta  <->  ps )
)
4 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
53, 4bitr4d 189 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  inimasn  4771  dmfco  5273  ltanqg  6652  genpassl  6776  genpassu  6777  ltexprlemloc  6859  caucvgprlemcanl  6896  cauappcvgprlemladdrl  6909  caucvgprlemladdrl  6930  caucvgprprlemaddq  6960  apneg  7778  lemuldiv  8026  msq11  8047  negiso  8100  avglt2  8337  iooshf  9051  qtri3or  9329  sq11ap  9736  sizeen  9808  sizedom  9827  cjap  9931  sqrt11ap  10062  clim2c  10261  climabs0  10284  nndivides  10347  oddnn02np1  10424  oddge22np1  10425  evennn02n  10426  evennn2n  10427  halfleoddlt  10438
  Copyright terms: Public domain W3C validator