Theorem sylan9r 517

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  3orel13  1511  spimt  2420  euim  2647  ceqsalt  3490  spcimgft  3517  axprlem3OLD  5391  feldmfvelcdm  7071  limsssuc  7834  tfindsg  7845  findsg  7882  f1oweALT  7957  oaordi  8519  pssnn  9141  inf3lem2  9586  updjudhf  9905  cardlim  9946  ac10ct  10006  cardaleph  10061  cfub  10220  cfcoflem  10244  hsmexlem2  10399  zorn2lem7  10474  pwcfsdom  10556  grur1a  10792  genpcd  10979  supadd  12174  supmul  12178  zeo  12673  uzwo  12926  xrub  13329  iccsupr  13460  reuccatpfxs1lem  14773  climuni  15593  efgi2  19786  opnnei  23238  tgcn  23370  locfincf  23649  uffix  24039  alexsubALTlem2  24166  alexsubALT  24169  metrest  24642  causs  25418  ocin  31557  spanuni  31805  superpos  32615  bnj518  35191  nndivsub  36830  bj-spimtv  37291  bj-snmoore  37615  cover2  38226  metf1o  38266  sn-axprlem3  42849  intabssd  44107  relpfrlem  45527  stoweidlem62  46634  pgindnf  50345