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  2388  euim  2614  ceqsalt  3471  spcimgft  3500  axprlem3OLD  5368  feldmfvelcdm  7025  limsssuc  7786  tfindsg  7797  findsg  7833  f1oweALT  7910  oaordi  8467  pssnn  9085  inf3lem2  9526  updjudhf  9831  cardlim  9872  ac10ct  9932  cardaleph  9987  cfub  10147  cfcoflem  10170  hsmexlem2  10325  zorn2lem7  10400  pwcfsdom  10481  grur1a  10717  genpcd  10904  supadd  12097  supmul  12101  zeo  12565  uzwo  12811  xrub  13213  iccsupr  13344  reuccatpfxs1lem  14655  climuni  15461  efgi2  19639  opnnei  23036  tgcn  23168  locfincf  23447  uffix  23837  alexsubALTlem2  23964  alexsubALT  23967  metrest  24440  causs  25226  ocin  31278  spanuni  31526  superpos  32336  bnj518  34919  nndivsub  36522  bj-spimtv  36859  bj-snmoore  37178  cover2  37776  metf1o  37816  sn-axprlem3  42336  intabssd  43637  relpfrlem  45071  stoweidlem62  46185  pgindnf  49842