Theorem sylan9r 511

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  spimt  2404  euim  2701  axprlem3  5326  limsssuc  7565  tfindsg  7575  findsg  7609  f1oweALT  7673  oaordi  8172  pssnn  8736  inf3lem2  9092  updjudhf  9360  cardlim  9401  ac10ct  9460  cardaleph  9515  cfub  9671  cfcoflem  9694  hsmexlem2  9849  zorn2lem7  9924  pwcfsdom  10005  grur1a  10241  genpcd  10428  supadd  11609  supmul  11613  zeo  12069  uzwo  12312  xrub  12706  iccsupr  12831  reuccatpfxs1lem  14108  climuni  14909  efgi2  18851  opnnei  21728  tgcn  21860  locfincf  22139  uffix  22529  alexsubALTlem2  22656  alexsubALT  22659  metrest  23134  causs  23901  ocin  29073  spanuni  29321  superpos  30131  bnj518  32158  3orel13  32947  trpredmintr  33070  frmin  33084  nndivsub  33805  bj-spimtv  34116  bj-snmoore  34408  cover2  35004  metf1o  35045  sn-axprlem3  39129  intabssd  39905  stoweidlem62  42367