Theorem sylan9r 518

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 79	. 2 ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏)))
4	3	imp 412	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3orel13  1517  spimt  2415  euim  2642  ceqsalt  3483  spcimgft  3510  feldmfvelcdm  7086  limsssuc  7861  tfindsg  7872  findsg  7909  f1oweALT  7984  oaordi  8557  pssnn  9187  inf3lem2  9633  updjudhf  10015  cardlim  10056  ac10ct  10116  cardaleph  10171  cfub  10329  cfcoflem  10353  hsmexlem2  10508  zorn2lem7  10583  pwcfsdom  10671  grur1a  10907  genpcd  11094  supadd  12288  supmul  12292  zeo  12788  uzwo  13041  xrub  13445  iccsupr  13576  reuccatpfxs1lem  14899  climuni  15724  efgi2  19944  opnnei  23443  tgcn  23575  locfincf  23855  uffix  24245  alexsubALTlem2  24372  alexsubALT  24375  metrest  24848  causs  25624  ocin  31903  spanuni  32151  superpos  32961  bnj518  35562  dfac16  35810  nndivsub  37337  bj-spimtv  37798  bj-snmoore  38126  cover2  38742  metf1o  38782  sn-axprlem3  43365  intabssd  44613  relpfrlem  46036  stoweidlem62  47165  pgindnf  50977