Theorem sylan9r 508

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 406	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  3orel13  1486  spimt  2384  euim  2612  ceqsalt  3505  axprlem3  5423  limsssuc  7843  tfindsg  7854  findsg  7894  f1oweALT  7963  oaordi  8552  pssnn  9174  pssnnOLD  9271  inf3lem2  9630  updjudhf  9932  cardlim  9973  ac10ct  10035  cardaleph  10090  cfub  10250  cfcoflem  10273  hsmexlem2  10428  zorn2lem7  10503  pwcfsdom  10584  grur1a  10820  genpcd  11007  supadd  12189  supmul  12193  zeo  12655  uzwo  12902  xrub  13298  iccsupr  13426  reuccatpfxs1lem  14703  climuni  15503  efgi2  19641  opnnei  22944  tgcn  23076  locfincf  23355  uffix  23745  alexsubALTlem2  23872  alexsubALT  23875  metrest  24353  causs  25146  ocin  30982  spanuni  31230  superpos  32040  bnj518  34361  nndivsub  35806  bj-spimtv  36136  bj-snmoore  36458  cover2  37047  metf1o  37087  sn-axprlem3  41501  intabssd  42733  stoweidlem62  45237  pgindnf  47923