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  2421  euim  2648  ceqsalt  3491  spcimgft  3518  axprlem3OLD  5405  feldmfvelcdm  7088  limsssuc  7855  tfindsg  7866  findsg  7903  f1oweALT  7978  oaordi  8540  pssnn  9163  inf3lem2  9608  updjudhf  9936  cardlim  9977  ac10ct  10037  cardaleph  10092  cfub  10250  cfcoflem  10274  hsmexlem2  10429  zorn2lem7  10504  pwcfsdom  10586  grur1a  10822  genpcd  11009  supadd  12201  supmul  12205  zeo  12700  uzwo  12953  xrub  13356  iccsupr  13487  reuccatpfxs1lem  14807  climuni  15629  efgi2  19826  opnnei  23314  tgcn  23446  locfincf  23725  uffix  24115  alexsubALTlem2  24242  alexsubALT  24245  metrest  24718  causs  25494  ocin  31685  spanuni  31933  superpos  32743  bnj518  35306  nndivsub  37009  bj-spimtv  37470  bj-snmoore  37796  cover2  38407  metf1o  38447  sn-axprlem3  43030  intabssd  44286  relpfrlem  45703  stoweidlem62  46817  pgindnf  50535