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  908  nfimd  1895  axc15  2444  ax9ALT  2819  rspcimdv  3615  peano5  7607  isf34lem6  9804  inar1  10199  supsrlem  10535  r19.29uz  14712  o1of2  14971  o1rlimmul  14977  caucvg  15037  isprm5  16053  mrissmrid  16914  kgen2ss  22165  txlm  22258  isr0  22347  metcnpi3  23158  addcnlem  23474  nmhmcn  23726  aalioulem5  24927  xrlimcnp  25548  dmdmd  30079  mdsl0  30089  mdsl1i  30100  lmxrge0  31197  bnj517  32159  ax8dfeq  33045  poimirlem29  34923  heicant  34929  ispridlc  35350  dffltz  39278  intabssd  39892  ss2iundf  40011