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

Theorem 3bitr2d 215
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
3bitr2d  |-  ( ph  ->  ( ps  <->  ta )
)

Proof of Theorem 3bitr2d
StepHypRef Expression
1 3bitr2d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 3bitr2d.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
31, 2bitr4d 190 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 187 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ceqsralt  2685  frecsuclem  6269  indpi  7114  cauappcvgprlemladdru  7428  prsrlt  7559  lesub2  8183  ltsub2  8185  rec11ap  8430  avglt1  8909  rpnegap  9422  modqmuladdnn0  10081  expap0  10263  2shfti  10543  mulreap  10576  minmax  10941  lemininf  10945  xrminmax  10974  xrlemininf  10980  modremain  11522  nn0seqcvgd  11618  divgcdcoprm0  11678  isxmet2d  12412  xblss2  12469  neibl  12555  ellimc3apf  12672
  Copyright terms: Public domain W3C validator