Theorem sylan9r 509

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  3orel13  1487  spimt  2385  euim  2613  ceqsalt  3505  axprlem3  5423  limsssuc  7838  tfindsg  7849  findsg  7889  f1oweALT  7958  oaordi  8545  pssnn  9167  pssnnOLD  9264  inf3lem2  9623  updjudhf  9925  cardlim  9966  ac10ct  10028  cardaleph  10083  cfub  10243  cfcoflem  10266  hsmexlem2  10421  zorn2lem7  10496  pwcfsdom  10577  grur1a  10813  genpcd  11000  supadd  12181  supmul  12185  zeo  12647  uzwo  12894  xrub  13290  iccsupr  13418  reuccatpfxs1lem  14695  climuni  15495  efgi2  19592  opnnei  22623  tgcn  22755  locfincf  23034  uffix  23424  alexsubALTlem2  23551  alexsubALT  23554  metrest  24032  causs  24814  ocin  30544  spanuni  30792  superpos  31602  bnj518  33892  nndivsub  35337  bj-spimtv  35667  bj-snmoore  35989  cover2  36578  metf1o  36618  sn-axprlem3  41036  intabssd  42260  stoweidlem62  44768  pgindnf  47751