Theorem sylan9r 687

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

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  spimt  2240  limsssuc  6919  tfindsg  6929  findsg  6962  f1oweALT  7020  oaordi  7490  pssnn  8040  inf3lem2  8386  cardlim  8658  ac10ct  8717  cardaleph  8772  cfub  8931  cfcoflem  8954  hsmexlem2  9109  zorn2lem7  9184  pwcfsdom  9261  grur1a  9497  genpcd  9684  supadd  10838  supmul  10842  zeo  11295  uzwo  11583  xrub  11970  iccsupr  12093  reuccats1lem  13277  climuni  14077  efgi2  17907  opnnei  20676  tgcn  20808  locfincf  21086  uffix  21477  alexsubALTlem2  21604  alexsubALT  21607  metrest  22080  causs  22822  ocin  27345  spanuni  27593  superpos  28403  bnj518  30016  3orel13  30659  trpredmintr  30781  frmin  30789  nndivsub  31432  bj-spimtv  31711  cover2  32474  metf1o  32517  intabssd  36731  stoweidlem62  38752  reuccatpfxs1lem  40094