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  1518  spimt  2418  euim  2645  ceqsalt  3487  spcimgft  3514  feldmfvelcdm  7113  limsssuc  7888  tfindsg  7899  findsg  7936  f1oweALT  8011  oaordi  8585  pssnn  9215  inf3lem2  9660  updjudhf  10042  cardlim  10083  ac10ct  10143  cardaleph  10198  cfub  10356  cfcoflem  10380  hsmexlem2  10535  zorn2lem7  10610  pwcfsdom  10698  grur1a  10934  genpcd  11121  supadd  12315  supmul  12319  zeo  12815  uzwo  13068  xrub  13472  iccsupr  13603  reuccatpfxs1lem  14926  climuni  15751  efgi2  19972  opnnei  23471  tgcn  23603  locfincf  23883  uffix  24273  alexsubALTlem2  24400  alexsubALT  24403  metrest  24876  causs  25652  ocin  31931  spanuni  32179  superpos  32989  bnj518  35599  dfac16  35859  nndivsub  37436  bj-spimtv  37897  bj-snmoore  38238  cover2  38854  metf1o  38892  sn-axprlem3  43476  intabssd  44723  relpfrlem  46149  stoweidlem62  47287  pgindnf  51099