Theorem sylan9 510

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 409	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ax8  2120  ax9  2128  rspc2  3631  rspc2v  3633  rspc3v  3636  copsexgw  5381  copsexg  5382  chfnrn  6819  fvcofneq  6859  ffnfv  6882  f1elima  7021  onint  7510  peano5  7605  f1oweALT  7673  smoel2  8000  pssnn  8736  fiint  8795  dffi2  8887  alephnbtwn  9497  cfcof  9696  zorn2lem7  9924  suplem1pr  10474  addsrpr  10497  mulsrpr  10498  cau3lem  14714  divalglem8  15751  efgi  18845  elfrlmbasn0  20907  locfincmp  22134  tx1stc  22258  fbunfip  22477  filuni  22493  ufileu  22527  rescncf  23505  shmodsi  29166  spanuni  29321  spansneleq  29347  mdi  30072  dmdi  30079  dmdi4  30084  funimass4f  30382  bj-ax89  34011  poimirlem32  34939  ffnafv  43390