Theorem sylan9 508

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ax8  2087  ax9  2095  rspc2  3570  rspc2v  3572  rspc3v  3575  copsexg  5273  chfnrn  6684  fvcofneq  6724  ffnfv  6745  f1elima  6886  onint  7366  peano5  7461  f1oweALT  7529  smoel2  7852  pssnn  8582  fiint  8641  dffi2  8733  alephnbtwn  9343  cfcof  9542  zorn2lem7  9770  suplem1pr  10320  addsrpr  10343  mulsrpr  10344  cau3lem  14548  divalglem8  15584  efgi  18572  elfrlmbasn0  20589  locfincmp  21818  tx1stc  21942  fbunfip  22161  filuni  22177  ufileu  22211  rescncf  23188  shmodsi  28857  spanuni  29012  spansneleq  29038  mdi  29763  dmdi  29770  dmdi4  29775  funimass4f  30072  bj-ax89  33610  poimirlem32  34455  ffnafv  42886