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  1895  axc15  2422  ax9ALT  2726  rspcimdv  3567  peano5  7823  isf34lem6  10268  inar1  10663  supsrlem  10999  r19.29uz  15255  o1of2  15517  o1rlimmul  15523  caucvg  15583  isprm5  16615  mrissmrid  17544  kgen2ss  23468  txlm  23561  isr0  23650  metcnpi3  24459  addcnlem  24778  nmhmcn  25045  aalioulem5  26269  xrlimcnp  26903  dmdmd  32275  mdsl0  32285  mdsl1i  32296  fldextrspunlsplem  33681  lmxrge0  33960  bnj517  34892  ax8dfeq  35831  in-ax8  36257  ss-ax8  36258  poimirlem29  37688  heicant  37694  ispridlc  38109  dffltz  42666  intabssd  43551  ss2iundf  43691  ismnushort  44333