Theorem sylan9r 509

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  spimt  2386  euim  2619  axprlem3  5348  limsssuc  7697  tfindsg  7707  findsg  7746  f1oweALT  7815  oaordi  8377  pssnn  8951  pssnnOLD  9040  inf3lem2  9387  updjudhf  9689  cardlim  9730  ac10ct  9790  cardaleph  9845  cfub  10005  cfcoflem  10028  hsmexlem2  10183  zorn2lem7  10258  pwcfsdom  10339  grur1a  10575  genpcd  10762  supadd  11943  supmul  11947  zeo  12406  uzwo  12651  xrub  13046  iccsupr  13174  reuccatpfxs1lem  14459  climuni  15261  efgi2  19331  opnnei  22271  tgcn  22403  locfincf  22682  uffix  23072  alexsubALTlem2  23199  alexsubALT  23202  metrest  23680  causs  24462  ocin  29658  spanuni  29906  superpos  30716  bnj518  32866  3orel13  33660  nndivsub  34646  bj-spimtv  34976  bj-snmoore  35284  cover2  35872  metf1o  35913  sn-axprlem3  40186  intabssd  41126  stoweidlem62  43603