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  2151  ax9  2159  spcimgft  3511  rspc2  3585  rspc2v  3587  rspc3v  3592  rspc4v  3596  rspc8v  3598  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  chfnrn  7046  fvcofneq  7091  ffnfv  7117  f1elima  7265  onint  7802  peano5  7903  f1oweALT  7982  smoel2  8364  pssnn  9177  php  9215  fiint  9311  dffi2  9408  alephnbtwn  10143  cfcof  10345  zorn2lem7  10573  suplem1pr  11130  addsrpr  11153  mulsrpr  11154  cau3lem  15515  divalglem8  16563  efgi  19926  elfrlmbasn0  22062  locfincmp  23838  tx1stc  23962  fbunfip  24181  filuni  24197  ufileu  24231  rescncf  25211  shmodsi  31984  spanuni  32139  spansneleq  32165  mdi  32890  dmdi  32897  dmdi4  32902  funimass4f  33224  tz9.1regs  35785  bj-ax89  37558  poimirlem32  38550  ffnafv  48210