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	⊢ (𝜑 → (𝜓 → 𝜒))
imim12d.2	⊢ (𝜑 → (𝜃 → 𝜏))

Assertion

Ref	Expression
imim12d	⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏)))

Proof of Theorem imim12d

Step	Hyp	Ref	Expression
1		imim12d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imim12d.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
3	2	imim2d 57	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜒 → 𝜏)))
4	1, 3	syl5d 73	1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏)))

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  orim12dALT  912  nfimd  1896  axc15  2427  ax9ALT  2732  rspcimdv  3568  peano5  7845  isf34lem6  10302  inar1  10698  supsrlem  11034  r19.29uz  15286  o1of2  15548  o1rlimmul  15554  caucvg  15614  isprm5  16646  mrissmrid  17576  kgen2ss  23511  txlm  23604  isr0  23693  metcnpi3  24502  addcnlem  24821  nmhmcn  25088  aalioulem5  26312  xrlimcnp  26946  dmdmd  32387  mdsl0  32397  mdsl1i  32408  fldextrspunlsplem  33850  lmxrge0  34129  bnj517  35060  ax8dfeq  36009  in-ax8  36437  ss-ax8  36438  poimirlem29  37894  heicant  37900  ispridlc  38315  dffltz  42986  intabssd  43869  ss2iundf  44009  ismnushort  44651