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  1894  axc15  2420  ax9ALT  2724  rspcimdv  3578  peano5  7869  isf34lem6  10333  inar1  10728  supsrlem  11064  r19.29uz  15317  o1of2  15579  o1rlimmul  15585  caucvg  15645  isprm5  16677  mrissmrid  17602  kgen2ss  23442  txlm  23535  isr0  23624  metcnpi3  24434  addcnlem  24753  nmhmcn  25020  aalioulem5  26244  xrlimcnp  26878  dmdmd  32229  mdsl0  32239  mdsl1i  32250  fldextrspunlsplem  33668  lmxrge0  33942  bnj517  34875  ax8dfeq  35786  in-ax8  36212  ss-ax8  36213  poimirlem29  37643  heicant  37649  ispridlc  38064  dffltz  42622  intabssd  43508  ss2iundf  43648  ismnushort  44290