Theorem sylan9r 688

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 76	. 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 196  df-an 385

This theorem is referenced by:  spimt  2241  limsssuc  6942  tfindsg  6952  findsg  6985  f1oweALT  7043  oaordi  7513  pssnn  8063  inf3lem2  8409  cardlim  8681  ac10ct  8740  cardaleph  8795  cfub  8954  cfcoflem  8977  hsmexlem2  9132  zorn2lem7  9207  pwcfsdom  9284  grur1a  9520  genpcd  9707  supadd  10868  supmul  10872  zeo  11339  uzwo  11627  xrub  12014  iccsupr  12137  reuccats1lem  13331  climuni  14131  efgi2  17961  opnnei  20734  tgcn  20866  locfincf  21144  uffix  21535  alexsubALTlem2  21662  alexsubALT  21665  metrest  22139  causs  22904  ocin  27539  spanuni  27787  superpos  28597  bnj518  30210  3orel13  30853  trpredmintr  30975  frmin  30983  nndivsub  31626  bj-spimtv  31905  cover2  32678  metf1o  32721  intabssd  36935  stoweidlem62  38955  reuccatpfxs1lem  40296