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  2391  euim  2617  ceqsalt  3515  spcimgft  3546  axprlem3OLD  5428  feldmfvelcdm  7106  limsssuc  7871  tfindsg  7882  findsg  7919  f1oweALT  7997  oaordi  8584  pssnn  9208  inf3lem2  9669  updjudhf  9971  cardlim  10012  ac10ct  10074  cardaleph  10129  cfub  10289  cfcoflem  10312  hsmexlem2  10467  zorn2lem7  10542  pwcfsdom  10623  grur1a  10859  genpcd  11046  supadd  12236  supmul  12240  zeo  12704  uzwo  12953  xrub  13354  iccsupr  13482  reuccatpfxs1lem  14784  climuni  15588  efgi2  19743  opnnei  23128  tgcn  23260  locfincf  23539  uffix  23929  alexsubALTlem2  24056  alexsubALT  24059  metrest  24537  causs  25332  ocin  31315  spanuni  31563  superpos  32373  bnj518  34900  nndivsub  36458  bj-spimtv  36795  bj-snmoore  37114  cover2  37722  metf1o  37762  sn-axprlem3  42256  intabssd  43532  relpfrlem  44974  stoweidlem62  46077  pgindnf  49235