Theorem sylan9r 518

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 79	. 2 ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏)))
4	3	imp 412	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3orel13  1518  spimt  2416  euim  2643  ceqsalt  3484  spcimgft  3511  feldmfvelcdm  7078  limsssuc  7850  tfindsg  7861  findsg  7898  f1oweALT  7973  oaordi  8538  pssnn  9168  inf3lem2  9614  updjudhf  9993  cardlim  10034  ac10ct  10094  cardaleph  10149  cfub  10307  cfcoflem  10331  hsmexlem2  10486  zorn2lem7  10561  pwcfsdom  10649  grur1a  10885  genpcd  11072  supadd  12266  supmul  12270  zeo  12766  uzwo  13019  xrub  13423  iccsupr  13554  reuccatpfxs1lem  14875  climuni  15699  efgi2  19919  opnnei  23418  tgcn  23550  locfincf  23830  uffix  24220  alexsubALTlem2  24347  alexsubALT  24350  metrest  24823  causs  25599  ocin  31880  spanuni  32128  superpos  32938  bnj518  35499  nndivsub  37215  bj-spimtv  37676  bj-snmoore  38002  cover2  38617  metf1o  38657  sn-axprlem3  43240  intabssd  44478  relpfrlem  45895  stoweidlem62  47016  pgindnf  50753