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  1490  spimt  2391  euim  2618  ceqsalt  3476  spcimgft  3505  axprlem3OLD  5375  feldmfvelcdm  7040  limsssuc  7802  tfindsg  7813  findsg  7849  f1oweALT  7926  oaordi  8483  pssnn  9105  inf3lem2  9550  updjudhf  9855  cardlim  9896  ac10ct  9956  cardaleph  10011  cfub  10171  cfcoflem  10194  hsmexlem2  10349  zorn2lem7  10424  pwcfsdom  10506  grur1a  10742  genpcd  10929  supadd  12122  supmul  12126  zeo  12590  uzwo  12836  xrub  13239  iccsupr  13370  reuccatpfxs1lem  14681  climuni  15487  efgi2  19666  opnnei  23076  tgcn  23208  locfincf  23487  uffix  23877  alexsubALTlem2  24004  alexsubALT  24007  metrest  24480  causs  25266  ocin  31383  spanuni  31631  superpos  32441  bnj518  35061  nndivsub  36670  bj-spimtv  37036  bj-snmoore  37360  cover2  37960  metf1o  38000  sn-axprlem3  42584  intabssd  43869  relpfrlem  45303  stoweidlem62  46414  pgindnf  50069