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  1489  spimt  2390  euim  2616  ceqsalt  3494  spcimgft  3525  axprlem3OLD  5398  feldmfvelcdm  7076  limsssuc  7845  tfindsg  7856  findsg  7893  f1oweALT  7971  oaordi  8558  pssnn  9182  inf3lem2  9643  updjudhf  9945  cardlim  9986  ac10ct  10048  cardaleph  10103  cfub  10263  cfcoflem  10286  hsmexlem2  10441  zorn2lem7  10516  pwcfsdom  10597  grur1a  10833  genpcd  11020  supadd  12210  supmul  12214  zeo  12679  uzwo  12927  xrub  13328  iccsupr  13459  reuccatpfxs1lem  14764  climuni  15568  efgi2  19706  opnnei  23058  tgcn  23190  locfincf  23469  uffix  23859  alexsubALTlem2  23986  alexsubALT  23989  metrest  24463  causs  25250  ocin  31277  spanuni  31525  superpos  32335  bnj518  34917  nndivsub  36475  bj-spimtv  36812  bj-snmoore  37131  cover2  37739  metf1o  37779  sn-axprlem3  42268  intabssd  43543  relpfrlem  44978  stoweidlem62  46091  pgindnf  49580