Theorem sylan9 515

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 77	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	imp 410	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  ax8  2148  ax9  2156  spcimgft  3514  rspc2  3590  rspc2v  3592  rspc3v  3597  rspc4v  3601  rspc8v  3603  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  chfnrn  7030  fvcofneq  7074  ffnfv  7100  f1elima  7247  onint  7773  peano5  7874  f1oweALT  7953  smoel2  8334  pssnn  9137  php  9175  fiint  9271  dffi2  9369  alephnbtwn  10027  cfcof  10231  zorn2lem7  10459  suplem1pr  11010  addsrpr  11033  mulsrpr  11034  cau3lem  15382  divalglem8  16434  efgi  19759  elfrlmbasn0  21812  locfincmp  23583  tx1stc  23707  fbunfip  23926  filuni  23942  ufileu  23976  rescncf  24956  shmodsi  31589  spanuni  31744  spansneleq  31770  mdi  32495  dmdi  32502  dmdi4  32507  funimass4f  32836  tz9.1regs  35427  bj-ax89  37148  poimirlem32  38148  ffnafv  47762