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  911  nfimd  1895  axc15  2424  ax9ALT  2728  rspcimdv  3563  peano5  7829  isf34lem6  10278  inar1  10673  supsrlem  11009  r19.29uz  15260  o1of2  15522  o1rlimmul  15528  caucvg  15588  isprm5  16620  mrissmrid  17549  kgen2ss  23471  txlm  23564  isr0  23653  metcnpi3  24462  addcnlem  24781  nmhmcn  25048  aalioulem5  26272  xrlimcnp  26906  dmdmd  32282  mdsl0  32292  mdsl1i  32303  fldextrspunlsplem  33707  lmxrge0  33986  bnj517  34918  ax8dfeq  35861  in-ax8  36289  ss-ax8  36290  poimirlem29  37709  heicant  37715  ispridlc  38130  dffltz  42752  intabssd  43636  ss2iundf  43776  ismnushort  44418