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

Theorem 3imtr3d 201
Description: More general version of 3imtr3i 199. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
Hypotheses
Ref Expression
3imtr3d.1  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
3imtr3d.3  |-  ( ph  ->  ( ch  <->  ta )
)
Assertion
Ref Expression
3imtr3d  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr3d
StepHypRef Expression
1 3imtr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
2 3imtr3d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 3imtr3d.3 . . 3  |-  ( ph  ->  ( ch  <->  ta )
)
42, 3sylibd 148 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbird 169 1  |-  ( ph  ->  ( th  ->  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:  f1imass  5753  fornex  6094  tposfn2  6245  eroveu  6604  ismkvnex  7131  indpi  7304  axcaucvglemres  7861  qsqeqor  10586  caucvgrelemcau  10944  m1dvdsndvds  12202  pcpremul  12247  pcaddlem  12292  pockthlem  12308  limccnpcntop  13438  sincosq1sgn  13541  sincosq2sgn  13542  subctctexmid  14034
  Copyright terms: Public domain W3C validator