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 207  df-an 396

This theorem is referenced by:  3orel13  1485  spimt  2388  euim  2614  ceqsalt  3512  spcimgft  3545  axprlem3OLD  5433  feldmfvelcdm  7105  limsssuc  7870  tfindsg  7881  findsg  7919  f1oweALT  7995  oaordi  8582  pssnn  9206  inf3lem2  9666  updjudhf  9968  cardlim  10009  ac10ct  10071  cardaleph  10126  cfub  10286  cfcoflem  10309  hsmexlem2  10464  zorn2lem7  10539  pwcfsdom  10620  grur1a  10856  genpcd  11043  supadd  12233  supmul  12237  zeo  12701  uzwo  12950  xrub  13350  iccsupr  13478  reuccatpfxs1lem  14780  climuni  15584  efgi2  19757  opnnei  23143  tgcn  23275  locfincf  23554  uffix  23944  alexsubALTlem2  24071  alexsubALT  24074  metrest  24552  causs  25345  ocin  31324  spanuni  31572  superpos  32382  bnj518  34878  nndivsub  36439  bj-spimtv  36776  bj-snmoore  37095  cover2  37701  metf1o  37741  sn-axprlem3  42234  intabssd  43508  stoweidlem62  46017  pgindnf  48946