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

Theorem 3imtr4d 202
Description: More general version of 3imtr4i 200. 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 168 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 149 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:  onsucelsucr  4430  unielrel  5072  ovmpos  5900  caofrss  6012  caoftrn  6013  f1o2ndf1  6131  nnaord  6411  nnmord  6419  oviec  6541  pmss12g  6575  fiss  6871  pm54.43  7061  ltsopi  7150  lttrsr  7592  ltsosr  7594  aptisr  7609  mulextsr1  7611  axpre-mulext  7718  axltwlin  7854  axlttrn  7855  axltadd  7856  axmulgt0  7858  letr  7869  eqord1  8267  remulext1  8383  mulext1  8396  recexap  8436  prodge0  8634  lt2msq  8666  nnge1  8765  zltp1le  9130  uzss  9368  eluzp1m1  9371  xrletr  9619  ixxssixx  9713  zesq  10439  expcanlem  10491  expcan  10492  nn0opthd  10498  maxleast  11015  climshftlemg  11101  dvds1lem  11533  bezoutlemzz  11719  algcvg  11758  eucalgcvga  11768  rpexp12i  11862  crth  11929  tgss  12264  neipsm  12355  ssrest  12383  cos11  12975
  Copyright terms: Public domain W3C validator