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  909  nfimd  1897  axc15  2422  ax9ALT  2733  rspcimdv  3551  peano5  7740  peano5OLD  7741  isf34lem6  10136  inar1  10531  supsrlem  10867  r19.29uz  15062  o1of2  15322  o1rlimmul  15328  caucvg  15390  isprm5  16412  mrissmrid  17350  kgen2ss  22706  txlm  22799  isr0  22888  metcnpi3  23702  addcnlem  24027  nmhmcn  24283  aalioulem5  25496  xrlimcnp  26118  dmdmd  30662  mdsl0  30672  mdsl1i  30683  lmxrge0  31902  bnj517  32865  ax8dfeq  33774  poimirlem29  35806  heicant  35812  ispridlc  36228  dffltz  40471  intabssd  41126  ss2iundf  41267  ismnushort  41919