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

This theorem is referenced by:  spimt  2386  euim  2619  axprlem3  5343  limsssuc  7672  tfindsg  7682  findsg  7720  f1oweALT  7788  oaordi  8339  pssnn  8913  pssnnOLD  8969  inf3lem2  9317  trpredmintr  9409  frmin  9438  updjudhf  9620  cardlim  9661  ac10ct  9721  cardaleph  9776  cfub  9936  cfcoflem  9959  hsmexlem2  10114  zorn2lem7  10189  pwcfsdom  10270  grur1a  10506  genpcd  10693  supadd  11873  supmul  11877  zeo  12336  uzwo  12580  xrub  12975  iccsupr  13103  reuccatpfxs1lem  14387  climuni  15189  efgi2  19246  opnnei  22179  tgcn  22311  locfincf  22590  uffix  22980  alexsubALTlem2  23107  alexsubALT  23110  metrest  23586  causs  24367  ocin  29559  spanuni  29807  superpos  30617  bnj518  32766  3orel13  33562  nndivsub  34573  bj-spimtv  34903  bj-snmoore  35211  cover2  35799  metf1o  35840  sn-axprlem3  40114  intabssd  41024  stoweidlem62  43493