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  2384  euim  2610  ceqsalt  3472  spcimgft  3503  axprlem3OLD  5370  feldmfvelcdm  7024  limsssuc  7790  tfindsg  7801  findsg  7837  f1oweALT  7914  oaordi  8471  pssnn  9092  inf3lem2  9544  updjudhf  9846  cardlim  9887  ac10ct  9947  cardaleph  10002  cfub  10162  cfcoflem  10185  hsmexlem2  10340  zorn2lem7  10415  pwcfsdom  10496  grur1a  10732  genpcd  10919  supadd  12111  supmul  12115  zeo  12580  uzwo  12830  xrub  13232  iccsupr  13363  reuccatpfxs1lem  14670  climuni  15477  efgi2  19622  opnnei  23023  tgcn  23155  locfincf  23434  uffix  23824  alexsubALTlem2  23951  alexsubALT  23954  metrest  24428  causs  25214  ocin  31258  spanuni  31506  superpos  32316  bnj518  34852  nndivsub  36430  bj-spimtv  36767  bj-snmoore  37086  cover2  37694  metf1o  37734  sn-axprlem3  42190  intabssd  43492  relpfrlem  44927  stoweidlem62  46044  pgindnf  49702