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  910  nfimd  1897  axc15  2420  ax9ALT  2726  rspcimdv  3572  peano5  7835  peano5OLD  7836  isf34lem6  10325  inar1  10720  supsrlem  11056  r19.29uz  15247  o1of2  15507  o1rlimmul  15513  caucvg  15575  isprm5  16594  mrissmrid  17535  kgen2ss  22943  txlm  23036  isr0  23125  metcnpi3  23939  addcnlem  24264  nmhmcn  24520  aalioulem5  25733  xrlimcnp  26355  dmdmd  31305  mdsl0  31315  mdsl1i  31326  lmxrge0  32622  bnj517  33586  ax8dfeq  34459  poimirlem29  36180  heicant  36186  ispridlc  36602  dffltz  41030  intabssd  41913  ss2iundf  42053  ismnushort  42703