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

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

Proof of Theorem 3imtr4d
StepHypRef Expression
1 3imtr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
2 3imtr4d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 3imtr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
42, 3sylibrd 167 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 148 1  |-  ( ph  ->  ( th  ->  ta ) )
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:  onsucelsucr  4260  unielrel  4875  ovmpt2s  5655  caofrss  5766  caoftrn  5767  f1o2ndf1  5880  nnaord  6148  nnmord  6156  oviec  6278  pm54.43  6518  ltsopi  6572  lttrsr  7001  ltsosr  7003  aptisr  7017  mulextsr1  7019  axpre-mulext  7116  axltwlin  7247  axlttrn  7248  axltadd  7249  axmulgt0  7251  letr  7261  remulext1  7766  mulext1  7779  recexap  7810  prodge0  7999  lt2msq  8031  nnge1  8129  zltp1le  8486  uzss  8720  eluzp1m1  8723  xrletr  8954  ixxssixx  9001  zesq  9688  expcanlem  9740  expcan  9741  nn0opthd  9746  maxleast  10237  climshftlemg  10279  dvds1lem  10351  bezoutlemzz  10535  ialgcvg  10574  eucialgcvga  10584  rpexp12i  10678
  Copyright terms: Public domain W3C validator