Theorem sylan9r 510

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem sylan9r

Step	Hyp	Ref	Expression
1		sylan9r.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylan9r.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9r 78	. 2 ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏)))
4	3	imp 408	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  3orel13  1488  spimt  2386  euim  2614  ceqsalt  3506  axprlem3  5424  limsssuc  7839  tfindsg  7850  findsg  7890  f1oweALT  7959  oaordi  8546  pssnn  9168  pssnnOLD  9265  inf3lem2  9624  updjudhf  9926  cardlim  9967  ac10ct  10029  cardaleph  10084  cfub  10244  cfcoflem  10267  hsmexlem2  10422  zorn2lem7  10497  pwcfsdom  10578  grur1a  10814  genpcd  11001  supadd  12182  supmul  12186  zeo  12648  uzwo  12895  xrub  13291  iccsupr  13419  reuccatpfxs1lem  14696  climuni  15496  efgi2  19593  opnnei  22624  tgcn  22756  locfincf  23035  uffix  23425  alexsubALTlem2  23552  alexsubALT  23555  metrest  24033  causs  24815  ocin  30549  spanuni  30797  superpos  31607  bnj518  33897  nndivsub  35342  bj-spimtv  35672  bj-snmoore  35994  cover2  36583  metf1o  36623  sn-axprlem3  41034  intabssd  42270  stoweidlem62  44778  pgindnf  47761