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  2153  ax9  2161  spcimgft  3514  rspc2  3588  rspc2v  3590  rspc3v  3595  rspc4v  3599  rspc8v  3601  copsexgw  5467  copsexgwOLD  5468  copsexg  5469  cotsexgw  5470  ssrel  5767  chfnrn  7079  fvcofneq  7125  ffnfv  7151  f1elima  7298  onint  7838  peano5  7939  f1oweALT  8018  smoel2  8409  pssnn  9222  php  9260  fiint  9356  dffi2  9452  alephnbtwn  10189  cfcof  10391  zorn2lem7  10619  suplem1pr  11176  addsrpr  11199  mulsrpr  11200  cau3lem  15566  divalglem8  16614  efgi  19984  elfrlmbasn0  22124  locfincmp  23900  tx1stc  24024  fbunfip  24243  filuni  24259  ufileu  24293  rescncf  25273  shmodsi  32048  spanuni  32203  spansneleq  32229  mdi  32954  dmdi  32961  dmdi4  32966  funimass4f  33329  dfac16  35887  tz9.1regs  35943  bj-ax89  37793  bj-ssrel  38175  poimirlem32  38838  ffnafv  48514