Theorem sylan9 517

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
sylan9.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylan9.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
sylan9	⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylan9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9 78	. 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:  ax8  2150  ax9  2158  spcimgft  3510  rspc2  3584  rspc2v  3586  rspc3v  3591  rspc4v  3595  rspc8v  3597  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  chfnrn  7053  fvcofneq  7098  ffnfv  7124  f1elima  7271  onint  7808  peano5  7909  f1oweALT  7988  smoel2  8378  pssnn  9191  php  9229  fiint  9325  dffi2  9422  alephnbtwn  10157  cfcof  10359  zorn2lem7  10587  suplem1pr  11144  addsrpr  11167  mulsrpr  11168  cau3lem  15531  divalglem8  16579  efgi  19942  elfrlmbasn0  22078  locfincmp  23854  tx1stc  23978  fbunfip  24197  filuni  24213  ufileu  24247  rescncf  25227  shmodsi  32000  spanuni  32155  spansneleq  32181  mdi  32906  dmdi  32913  dmdi4  32918  funimass4f  33282  dfac16  35814  tz9.1regs  35862  bj-ax89  37674  poimirlem32  38679  ffnafv  48349