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  917  nfimd  1901  axc15  2430  ax9ALT  2735  rspcimdv  3557  peano5  7840  isf34lem6  10300  inar1  10696  supsrlem  11032  r19.29uz  15311  o1of2  15573  o1rlimmul  15579  caucvg  15639  isprm5  16675  mrissmrid  17605  kgen2ss  23545  txlm  23638  isr0  23727  metcnpi3  24536  addcnlem  24855  nmhmcn  25112  aalioulem5  26327  xrlimcnp  26957  dmdmd  32396  mdsl0  32406  mdsl1i  32417  fldextrspunlsplem  33864  lmxrge0  34143  bnj517  35074  axpowg2  35335  axpowg3  35336  ax8dfeq  36031  in-ax8  36459  ss-ax8  36460  wl-dfcleq  37883  poimirlem29  38023  heicant  38029  ispridlc  38444  dffltz  43091  intabssd  43970  ss2iundf  44110  ismnushort  44752