Theorem sylan9 507

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 77	. 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:  ax8  2120  ax9  2128  spcimgft  3491  rspc2  3573  rspc2v  3575  rspc3v  3580  rspc4v  3584  rspc8v  3586  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  chfnrn  7001  fvcofneq  7045  ffnfv  7071  f1elima  7218  onint  7744  peano5  7844  f1oweALT  7925  smoel2  8303  pssnn  9103  php  9141  fiint  9237  dffi2  9336  alephnbtwn  9993  cfcof  10196  zorn2lem7  10424  suplem1pr  10975  addsrpr  10998  mulsrpr  10999  cau3lem  15317  divalglem8  16369  efgi  19694  elfrlmbasn0  21743  locfincmp  23491  tx1stc  23615  fbunfip  23834  filuni  23850  ufileu  23884  rescncf  24864  shmodsi  31460  spanuni  31615  spansneleq  31641  mdi  32366  dmdi  32373  dmdi4  32378  funimass4f  32710  tz9.1regs  35278  bj-ax89  36973  poimirlem32  37973  ffnafv  47619