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  2417  euim  2644  ceqsalt  3486  spcimgft  3513  axprlem3OLD  5398  feldmfvelcdm  7083  limsssuc  7850  tfindsg  7861  findsg  7898  f1oweALT  7973  oaordi  8537  pssnn  9167  inf3lem2  9612  updjudhf  9940  cardlim  9981  ac10ct  10041  cardaleph  10096  cfub  10254  cfcoflem  10278  hsmexlem2  10433  zorn2lem7  10508  pwcfsdom  10596  grur1a  10832  genpcd  11019  supadd  12211  supmul  12215  zeo  12711  uzwo  12964  xrub  13368  iccsupr  13499  reuccatpfxs1lem  14819  climuni  15643  efgi2  19858  opnnei  23351  tgcn  23483  locfincf  23763  uffix  24153  alexsubALTlem2  24280  alexsubALT  24283  metrest  24756  causs  25532  ocin  31785  spanuni  32033  superpos  32843  bnj518  35403  nndivsub  37084  bj-spimtv  37545  bj-snmoore  37871  cover2  38473  metf1o  38513  sn-axprlem3  43096  intabssd  44367  relpfrlem  45784  stoweidlem62  46898  pgindnf  50650