Theorem sylan9 509

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ax8  2113  ax9  2121  rspc2  3587  rspc2v  3589  rspc3v  3592  copsexgw  5445  copsexg  5446  chfnrn  6995  fvcofneq  7038  ffnfv  7061  f1elima  7205  onint  7716  peano5  7821  peano5OLD  7822  f1oweALT  7896  smoel2  8277  pssnn  9046  php  9088  pssnnOLD  9143  fiint  9202  dffi2  9293  alephnbtwn  9941  cfcof  10144  zorn2lem7  10372  suplem1pr  10922  addsrpr  10945  mulsrpr  10946  cau3lem  15175  divalglem8  16218  efgi  19436  elfrlmbasn0  21098  locfincmp  22805  tx1stc  22929  fbunfip  23148  filuni  23164  ufileu  23198  rescncf  24188  shmodsi  30136  spanuni  30291  spansneleq  30317  mdi  31042  dmdi  31049  dmdi4  31054  funimass4f  31355  bj-ax89  35073  poimirlem32  36041  ffnafv  45194