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  2637  axprlem3  5297  limsssuc  7569  tfindsg  7579  findsg  7614  f1oweALT  7682  oaordi  8187  pssnn  8743  pssnnOLD  8779  inf3lem2  9130  updjudhf  9398  cardlim  9439  ac10ct  9499  cardaleph  9554  cfub  9714  cfcoflem  9737  hsmexlem2  9892  zorn2lem7  9967  pwcfsdom  10048  grur1a  10284  genpcd  10471  supadd  11650  supmul  11654  zeo  12112  uzwo  12356  xrub  12751  iccsupr  12879  reuccatpfxs1lem  14160  climuni  14962  efgi2  18923  opnnei  21825  tgcn  21957  locfincf  22236  uffix  22626  alexsubALTlem2  22753  alexsubALT  22756  metrest  23231  causs  24003  ocin  29183  spanuni  29431  superpos  30241  bnj518  32390  3orel13  33182  trpredmintr  33321  frmin  33338  nndivsub  34221  bj-spimtv  34538  bj-snmoore  34834  cover2  35458  metf1o  35499  sn-axprlem3  39729  intabssd  40628  stoweidlem62  43098