Theorem sylan9r 517

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 411	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  3orel13  1518  spimt  2418  euim  2645  ceqsalt  3488  spcimgft  3515  axprlem3OLD  5402  feldmfvelcdm  7083  limsssuc  7847  tfindsg  7858  findsg  7895  f1oweALT  7970  oaordi  8532  pssnn  9154  inf3lem2  9599  updjudhf  9918  cardlim  9959  ac10ct  10019  cardaleph  10074  cfub  10233  cfcoflem  10257  hsmexlem2  10412  zorn2lem7  10487  pwcfsdom  10569  grur1a  10805  genpcd  10992  supadd  12184  supmul  12188  zeo  12683  uzwo  12936  xrub  13339  iccsupr  13470  reuccatpfxs1lem  14785  climuni  15605  efgi2  19796  opnnei  23258  tgcn  23390  locfincf  23669  uffix  24059  alexsubALTlem2  24186  alexsubALT  24189  metrest  24662  causs  25438  ocin  31626  spanuni  31874  superpos  32684  bnj518  35252  nndivsub  36946  bj-spimtv  37407  bj-snmoore  37733  cover2  38344  metf1o  38384  sn-axprlem3  42967  intabssd  44225  relpfrlem  45642  stoweidlem62  46756  pgindnf  50471