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  4849  dmfco  5372  ltanqg  6959  genpassl  7083  genpassu  7084  ltexprlemloc  7166  caucvgprlemcanl  7203  cauappcvgprlemladdrl  7216  caucvgprlemladdrl  7237  caucvgprprlemaddq  7267  apneg  8088  lemuldiv  8342  msq11  8363  negiso  8416  avglt2  8655  iooshf  9370  qtri3or  9654  sq11ap  10120  hashen  10192  fihashdom  10211  cjap  10340  sqrt11ap  10471  clim2c  10672  climabs0  10696  absefib  11060  efieq1re  11061  nndivides  11081  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161  halfleoddlt  11172
  Copyright terms: Public domain W3C validator