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  1486  spimt  2394  euim  2620  ceqsalt  3523  spcimgft  3558  axprlem3  5443  feldmfvelcdm  7120  limsssuc  7887  tfindsg  7898  findsg  7937  f1oweALT  8013  oaordi  8602  pssnn  9234  inf3lem2  9698  updjudhf  10000  cardlim  10041  ac10ct  10103  cardaleph  10158  cfub  10318  cfcoflem  10341  hsmexlem2  10496  zorn2lem7  10571  pwcfsdom  10652  grur1a  10888  genpcd  11075  supadd  12263  supmul  12267  zeo  12729  uzwo  12976  xrub  13374  iccsupr  13502  reuccatpfxs1lem  14794  climuni  15598  efgi2  19767  opnnei  23149  tgcn  23281  locfincf  23560  uffix  23950  alexsubALTlem2  24077  alexsubALT  24080  metrest  24558  causs  25351  ocin  31328  spanuni  31576  superpos  32386  bnj518  34862  nndivsub  36423  bj-spimtv  36760  bj-snmoore  37079  cover2  37675  metf1o  37715  sn-axprlem3  42210  intabssd  43481  stoweidlem62  45983  pgindnf  48808