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  4298  unielrel  4924  ovmpt2s  5725  caofrss  5836  caoftrn  5837  f1o2ndf1  5950  nnaord  6220  nnmord  6228  oviec  6350  pmss12g  6384  pm54.43  6762  ltsopi  6823  lttrsr  7252  ltsosr  7254  aptisr  7268  mulextsr1  7270  axpre-mulext  7367  axltwlin  7498  axlttrn  7499  axltadd  7500  axmulgt0  7502  letr  7512  remulext1  8017  mulext1  8030  recexap  8061  prodge0  8250  lt2msq  8282  nnge1  8380  zltp1le  8737  uzss  8971  eluzp1m1  8974  xrletr  9205  ixxssixx  9252  zesq  9968  expcanlem  10020  expcan  10021  nn0opthd  10026  maxleast  10541  climshftlemg  10583  dvds1lem  10682  bezoutlemzz  10866  ialgcvg  10905  eucialgcvga  10915  rpexp12i  11009  crth  11075
  Copyright terms: Public domain W3C validator