Theorem sylan9r 512

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

This theorem is referenced by:  spimt  2393  euim  2678  axprlem3  5291  limsssuc  7545  tfindsg  7555  findsg  7590  f1oweALT  7655  oaordi  8155  pssnn  8720  inf3lem2  9076  updjudhf  9344  cardlim  9385  ac10ct  9445  cardaleph  9500  cfub  9660  cfcoflem  9683  hsmexlem2  9838  zorn2lem7  9913  pwcfsdom  9994  grur1a  10230  genpcd  10417  supadd  11596  supmul  11600  zeo  12056  uzwo  12299  xrub  12693  iccsupr  12820  reuccatpfxs1lem  14099  climuni  14901  efgi2  18843  opnnei  21725  tgcn  21857  locfincf  22136  uffix  22526  alexsubALTlem2  22653  alexsubALT  22656  metrest  23131  causs  23902  ocin  29079  spanuni  29327  superpos  30137  bnj518  32268  3orel13  33060  trpredmintr  33183  frmin  33197  nndivsub  33918  bj-spimtv  34231  bj-snmoore  34528  cover2  35152  metf1o  35193  sn-axprlem3  39401  intabssd  40227  stoweidlem62  42704