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  2384  euim  2610  ceqsalt  3481  spcimgft  3512  axprlem3OLD  5383  feldmfvelcdm  7058  limsssuc  7826  tfindsg  7837  findsg  7873  f1oweALT  7951  oaordi  8510  pssnn  9132  inf3lem2  9582  updjudhf  9884  cardlim  9925  ac10ct  9987  cardaleph  10042  cfub  10202  cfcoflem  10225  hsmexlem2  10380  zorn2lem7  10455  pwcfsdom  10536  grur1a  10772  genpcd  10959  supadd  12151  supmul  12155  zeo  12620  uzwo  12870  xrub  13272  iccsupr  13403  reuccatpfxs1lem  14711  climuni  15518  efgi2  19655  opnnei  23007  tgcn  23139  locfincf  23418  uffix  23808  alexsubALTlem2  23935  alexsubALT  23938  metrest  24412  causs  25198  ocin  31225  spanuni  31473  superpos  32283  bnj518  34876  nndivsub  36445  bj-spimtv  36782  bj-snmoore  37101  cover2  37709  metf1o  37749  sn-axprlem3  42205  intabssd  43508  relpfrlem  44943  stoweidlem62  46060  pgindnf  49705