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  1489  spimt  2385  euim  2611  ceqsalt  3484  spcimgft  3515  axprlem3OLD  5386  feldmfvelcdm  7061  limsssuc  7829  tfindsg  7840  findsg  7876  f1oweALT  7954  oaordi  8513  pssnn  9138  inf3lem2  9589  updjudhf  9891  cardlim  9932  ac10ct  9994  cardaleph  10049  cfub  10209  cfcoflem  10232  hsmexlem2  10387  zorn2lem7  10462  pwcfsdom  10543  grur1a  10779  genpcd  10966  supadd  12158  supmul  12162  zeo  12627  uzwo  12877  xrub  13279  iccsupr  13410  reuccatpfxs1lem  14718  climuni  15525  efgi2  19662  opnnei  23014  tgcn  23146  locfincf  23425  uffix  23815  alexsubALTlem2  23942  alexsubALT  23945  metrest  24419  causs  25205  ocin  31232  spanuni  31480  superpos  32290  bnj518  34883  nndivsub  36452  bj-spimtv  36789  bj-snmoore  37108  cover2  37716  metf1o  37756  sn-axprlem3  42212  intabssd  43515  relpfrlem  44950  stoweidlem62  46067  pgindnf  49709