Theorem sylan9 507

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  ax8  2105  ax9  2113  rspc2  3616  rspc2v  3618  rspc3v  3623  rspc4v  3626  rspc8v  3628  copsexgw  5486  copsexg  5487  chfnrn  7052  fvcofneq  7097  ffnfv  7123  f1elima  7267  onint  7787  peano5  7893  peano5OLD  7894  f1oweALT  7970  smoel2  8377  pssnn  9184  php  9226  pssnnOLD  9281  fiint  9340  dffi2  9438  alephnbtwn  10086  cfcof  10289  zorn2lem7  10517  suplem1pr  11067  addsrpr  11090  mulsrpr  11091  cau3lem  15325  divalglem8  16368  efgi  19665  elfrlmbasn0  21684  locfincmp  23417  tx1stc  23541  fbunfip  23760  filuni  23776  ufileu  23810  rescncf  24804  shmodsi  31186  spanuni  31341  spansneleq  31367  mdi  32092  dmdi  32099  dmdi4  32104  funimass4f  32405  bj-ax89  36090  poimirlem32  37060  ffnafv  46474