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  2390  euim  2617  ceqsalt  3463  spcimgft  3491  axprlem3OLD  5371  feldmfvelcdm  7038  limsssuc  7801  tfindsg  7812  findsg  7848  f1oweALT  7925  oaordi  8481  pssnn  9103  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  12124  supmul  12128  zeo  12615  uzwo  12861  xrub  13264  iccsupr  13395  reuccatpfxs1lem  14708  climuni  15514  efgi2  19700  opnnei  23085  tgcn  23217  locfincf  23496  uffix  23886  alexsubALTlem2  24013  alexsubALT  24016  metrest  24489  causs  25265  ocin  31367  spanuni  31615  superpos  32425  bnj518  35028  nndivsub  36639  bj-spimtv  37101  bj-snmoore  37425  cover2  38036  metf1o  38076  sn-axprlem3  42659  intabssd  43946  relpfrlem  45380  stoweidlem62  46490  pgindnf  50191