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  1490  spimt  2391  euim  2618  ceqsalt  3464  spcimgft  3492  axprlem3OLD  5366  feldmfvelcdm  7032  limsssuc  7794  tfindsg  7805  findsg  7841  f1oweALT  7918  oaordi  8474  pssnn  9096  inf3lem2  9541  updjudhf  9846  cardlim  9887  ac10ct  9947  cardaleph  10002  cfub  10162  cfcoflem  10185  hsmexlem2  10340  zorn2lem7  10415  pwcfsdom  10497  grur1a  10733  genpcd  10920  supadd  12115  supmul  12119  zeo  12606  uzwo  12852  xrub  13255  iccsupr  13386  reuccatpfxs1lem  14699  climuni  15505  efgi2  19691  opnnei  23095  tgcn  23227  locfincf  23506  uffix  23896  alexsubALTlem2  24023  alexsubALT  24026  metrest  24499  causs  25275  ocin  31382  spanuni  31630  superpos  32440  bnj518  35044  nndivsub  36655  bj-spimtv  37117  bj-snmoore  37441  cover2  38050  metf1o  38090  sn-axprlem3  42673  intabssd  43964  relpfrlem  45398  stoweidlem62  46508  pgindnf  50203