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  1898  axc15  2422  ax9ALT  2728  rspcimdv  3603  peano5  7884  peano5OLD  7885  isf34lem6  10375  inar1  10770  supsrlem  11106  r19.29uz  15297  o1of2  15557  o1rlimmul  15563  caucvg  15625  isprm5  16644  mrissmrid  17585  kgen2ss  23059  txlm  23152  isr0  23241  metcnpi3  24055  addcnlem  24380  nmhmcn  24636  aalioulem5  25849  xrlimcnp  26473  dmdmd  31553  mdsl0  31563  mdsl1i  31574  lmxrge0  32932  bnj517  33896  ax8dfeq  34770  poimirlem29  36517  heicant  36523  ispridlc  36938  dffltz  41376  intabssd  42270  ss2iundf  42410  ismnushort  43060