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  3621  rspc2v  3623  rspc3v  3628  rspc4v  3631  rspc8v  3633  copsexgw  5491  copsexg  5492  chfnrn  7051  fvcofneq  7095  ffnfv  7118  f1elima  7262  onint  7778  peano5  7884  peano5OLD  7885  f1oweALT  7959  smoel2  8363  pssnn  9168  php  9210  pssnnOLD  9265  fiint  9324  dffi2  9418  alephnbtwn  10066  cfcof  10269  zorn2lem7  10497  suplem1pr  11047  addsrpr  11070  mulsrpr  11071  cau3lem  15301  divalglem8  16343  efgi  19587  elfrlmbasn0  21318  locfincmp  23030  tx1stc  23154  fbunfip  23373  filuni  23389  ufileu  23423  rescncf  24413  shmodsi  30673  spanuni  30828  spansneleq  30854  mdi  31579  dmdi  31586  dmdi4  31591  funimass4f  31892  bj-ax89  35603  poimirlem32  36568  ffnafv  45927