Theorem sylan9r 507

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 405	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  3orel13  1485  spimt  2383  euim  2611  ceqsalt  3504  axprlem3  5422  limsssuc  7841  tfindsg  7852  findsg  7892  f1oweALT  7961  oaordi  8548  pssnn  9170  pssnnOLD  9267  inf3lem2  9626  updjudhf  9928  cardlim  9969  ac10ct  10031  cardaleph  10086  cfub  10246  cfcoflem  10269  hsmexlem2  10424  zorn2lem7  10499  pwcfsdom  10580  grur1a  10816  genpcd  11003  supadd  12186  supmul  12190  zeo  12652  uzwo  12899  xrub  13295  iccsupr  13423  reuccatpfxs1lem  14700  climuni  15500  efgi2  19634  opnnei  22844  tgcn  22976  locfincf  23255  uffix  23645  alexsubALTlem2  23772  alexsubALT  23775  metrest  24253  causs  25046  ocin  30816  spanuni  31064  superpos  31874  bnj518  34195  nndivsub  35645  bj-spimtv  35975  bj-snmoore  36297  cover2  36886  metf1o  36926  sn-axprlem3  41340  intabssd  42572  stoweidlem62  45076  pgindnf  47848