Theorem sylan9 687

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 75	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	imp 444	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ax8  1983  ax9  1990  rspc2  3292  rspc3v  3296  trintss  4697  copsexg  4882  chfnrn  6236  fvcofneq  6275  ffnfv  6295  f1elima  6421  onint  6887  peano5  6981  f1oweALT  7043  smoel2  7347  pssnn  8063  fiint  8122  dffi2  8212  alephnbtwn  8777  cfcof  8979  zorn2lem7  9207  suplem1pr  9753  addsrpr  9775  mulsrpr  9776  cau3lem  13942  divalglem8  14961  efgi  17955  elfrlmbasn0  19925  locfincmp  21139  tx1stc  21263  fbunfip  21483  filuni  21499  ufileu  21533  rescncf  22508  shmodsi  27632  spanuni  27787  spansneleq  27813  mdi  28538  dmdi  28545  dmdi4  28550  funimass4f  28818  bj-ax89  31854  poimirlem32  32611  ffnafv  39900