Theorem sylan9r 691

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  spimt  2289  limsssuc  7092  tfindsg  7102  findsg  7135  f1oweALT  7194  oaordi  7671  pssnn  8219  inf3lem2  8564  cardlim  8836  ac10ct  8895  cardaleph  8950  cfub  9109  cfcoflem  9132  hsmexlem2  9287  zorn2lem7  9362  pwcfsdom  9443  grur1a  9679  genpcd  9866  supadd  11029  supmul  11033  zeo  11501  uzwo  11789  xrub  12180  iccsupr  12304  reuccats1lem  13525  climuni  14327  efgi2  18184  opnnei  20972  tgcn  21104  locfincf  21382  uffix  21772  alexsubALTlem2  21899  alexsubALT  21902  metrest  22376  causs  23142  ocin  28283  spanuni  28531  superpos  29341  bnj518  31082  3orel13  31724  trpredmintr  31855  frmin  31867  nndivsub  32581  bj-spimtv  32843  bj-snmoore  33193  cover2  33638  metf1o  33681  intabssd  38233  stoweidlem62  40597  reuccatpfxs1lem  41758