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  2386  euim  2612  ceqsalt  3470  spcimgft  3501  axprlem3OLD  5366  feldmfvelcdm  7019  limsssuc  7780  tfindsg  7791  findsg  7827  f1oweALT  7904  oaordi  8461  pssnn  9078  inf3lem2  9519  updjudhf  9821  cardlim  9862  ac10ct  9922  cardaleph  9977  cfub  10137  cfcoflem  10160  hsmexlem2  10315  zorn2lem7  10390  pwcfsdom  10471  grur1a  10707  genpcd  10894  supadd  12087  supmul  12091  zeo  12556  uzwo  12806  xrub  13208  iccsupr  13339  reuccatpfxs1lem  14650  climuni  15456  efgi2  19635  opnnei  23033  tgcn  23165  locfincf  23444  uffix  23834  alexsubALTlem2  23961  alexsubALT  23964  metrest  24437  causs  25223  ocin  31271  spanuni  31519  superpos  32329  bnj518  34893  nndivsub  36490  bj-spimtv  36827  bj-snmoore  37146  cover2  37754  metf1o  37794  sn-axprlem3  42249  intabssd  43551  relpfrlem  44985  stoweidlem62  46099  pgindnf  49747