Theorem sylan9r 508

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3orel13  1489  spimt  2390  euim  2617  ceqsalt  3474  spcimgft  3503  axprlem3OLD  5373  feldmfvelcdm  7031  limsssuc  7792  tfindsg  7803  findsg  7839  f1oweALT  7916  oaordi  8473  pssnn  9093  inf3lem2  9538  updjudhf  9843  cardlim  9884  ac10ct  9944  cardaleph  9999  cfub  10159  cfcoflem  10182  hsmexlem2  10337  zorn2lem7  10412  pwcfsdom  10494  grur1a  10730  genpcd  10917  supadd  12110  supmul  12114  zeo  12578  uzwo  12824  xrub  13227  iccsupr  13358  reuccatpfxs1lem  14669  climuni  15475  efgi2  19654  opnnei  23064  tgcn  23196  locfincf  23475  uffix  23865  alexsubALTlem2  23992  alexsubALT  23995  metrest  24468  causs  25254  ocin  31371  spanuni  31619  superpos  32429  bnj518  35042  nndivsub  36651  bj-spimtv  36995  bj-snmoore  37314  cover2  37912  metf1o  37952  sn-axprlem3  42470  intabssd  43756  relpfrlem  45190  stoweidlem62  46302  pgindnf  49957