Theorem sylan9r 516

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  3orel13  1507  spimt  2416  euim  2643  ceqsalt  3486  spcimgft  3513  axprlem3OLD  5385  feldmfvelcdm  7063  limsssuc  7826  tfindsg  7837  findsg  7874  f1oweALT  7949  oaordi  8510  pssnn  9133  inf3lem2  9581  updjudhf  9886  cardlim  9927  ac10ct  9987  cardaleph  10042  cfub  10202  cfcoflem  10226  hsmexlem2  10381  zorn2lem7  10456  pwcfsdom  10538  grur1a  10774  genpcd  10961  supadd  12157  supmul  12161  zeo  12656  uzwo  12909  xrub  13312  iccsupr  13443  reuccatpfxs1lem  14756  climuni  15562  efgi2  19748  opnnei  23160  tgcn  23292  locfincf  23571  uffix  23961  alexsubALTlem2  24088  alexsubALT  24091  metrest  24564  causs  25340  ocin  31445  spanuni  31693  superpos  32503  bnj518  35145  nndivsub  36781  bj-spimtv  37243  bj-snmoore  37567  cover2  38178  metf1o  38218  sn-axprlem3  42801  intabssd  44059  relpfrlem  45493  stoweidlem62  46600  pgindnf  50301