Theorem sylan9r 513

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 208  df-an 397

This theorem is referenced by:  3orel13  1495  spimt  2394  euim  2621  ceqsalt  3466  spcimgft  3494  axprlem3OLD  5365  feldmfvelcdm  7034  limsssuc  7797  tfindsg  7808  findsg  7844  f1oweALT  7921  oaordi  8478  pssnn  9100  inf3lem2  9548  updjudhf  9853  cardlim  9894  ac10ct  9954  cardaleph  10009  cfub  10169  cfcoflem  10192  hsmexlem2  10347  zorn2lem7  10422  pwcfsdom  10504  grur1a  10740  genpcd  10927  supadd  12122  supmul  12126  zeo  12613  uzwo  12859  xrub  13262  iccsupr  13393  reuccatpfxs1lem  14706  climuni  15512  efgi2  19698  opnnei  23110  tgcn  23242  locfincf  23521  uffix  23911  alexsubALTlem2  24038  alexsubALT  24041  metrest  24514  causs  25290  ocin  31392  spanuni  31640  superpos  32450  bnj518  35075  nndivsub  36692  bj-spimtv  37154  bj-snmoore  37478  cover2  38089  metf1o  38129  sn-axprlem3  42712  intabssd  43970  relpfrlem  45404  stoweidlem62  46512  pgindnf  50213