Theorem sylan9 517

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
sylan9.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylan9.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
sylan9	⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylan9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9 78	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	imp 412	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ax8  2152  ax9  2160  spcimgft  3518  rspc2  3593  rspc2v  3595  rspc3v  3600  rspc4v  3604  rspc8v  3606  copsexgw  5477  copsexgwOLD  5478  copsexg  5479  chfnrn  7051  fvcofneq  7095  ffnfv  7121  f1elima  7268  onint  7798  peano5  7899  f1oweALT  7978  smoel2  8359  pssnn  9163  php  9201  fiint  9296  dffi2  9393  alephnbtwn  10074  cfcof  10276  zorn2lem7  10504  suplem1pr  11055  addsrpr  11078  mulsrpr  11079  cau3lem  15432  divalglem8  16483  efgi  19814  elfrlmbasn0  21943  locfincmp  23713  tx1stc  23837  fbunfip  24056  filuni  24072  ufileu  24106  rescncf  25086  shmodsi  31771  spanuni  31926  spansneleq  31952  mdi  32677  dmdi  32684  dmdi4  32689  funimass4f  33012  tz9.1regs  35563  bj-ax89  37334  poimirlem32  38336  ffnafv  47941