Theorem imim12d 81

Description: Deduction combining antecedents and consequents. Deduction associated with imim12 105 and imim12i 62. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. O'Cat, 30-Oct-2011.)

Hypotheses

Ref	Expression
imim12d.1	|- ( ph -> ( ps -> ch ) )
imim12d.2	|- ( ph -> ( th -> ta ) )

Assertion

Ref	Expression
imim12d	|- ( ph -> ( ( ch -> th ) -> ( ps -> ta ) ) )

Proof of Theorem imim12d

Step	Hyp	Ref	Expression
1		imim12d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		imim12d.2	. . 3 |- ( ph -> ( th -> ta ) )
3	2	imim2d 57	. 2 |- ( ph -> ( ( ch -> th ) -> ( ch -> ta ) ) )
4	1, 3	syl5d 73	1 |- ( ph -> ( ( ch -> th ) -> ( ps -> ta ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim1d  82  rspcimdv  3310  peano5  7089  isf34lem6  9202  inar1  9597  supsrlem  9932  r19.29uz  14090  o1of2  14343  o1rlimmul  14349  caucvg  14409  isprm5  15419  mrissmrid  16301  kgen2ss  21358  txlm  21451  isr0  21540  metcnpi3  22351  addcnlem  22667  nmhmcn  22920  aalioulem5  24091  xrlimcnp  24695  dmdmd  29159  mdsl0  29169  mdsl1i  29180  lmxrge0  29998  bnj517  30955  ax8dfeq  31704  bj-mo3OLD  32832  bj-ax9-2  32891  poimirlem29  33438  heicant  33444  ispridlc  33869  intabssd  37916  ss2iundf  37951