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

This theorem is referenced by:  ax8  2113  ax9  2121  rspc2  3569  rspc2v  3571  rspc3v  3574  copsexgw  5405  copsexg  5406  chfnrn  6935  fvcofneq  6978  ffnfv  7001  f1elima  7145  onint  7649  peano5  7749  peano5OLD  7750  f1oweALT  7824  smoel2  8203  pssnn  8960  php  9002  pssnnOLD  9049  fiint  9100  dffi2  9191  alephnbtwn  9836  cfcof  10039  zorn2lem7  10267  suplem1pr  10817  addsrpr  10840  mulsrpr  10841  cau3lem  15075  divalglem8  16118  efgi  19334  elfrlmbasn0  20979  locfincmp  22686  tx1stc  22810  fbunfip  23029  filuni  23045  ufileu  23079  rescncf  24069  shmodsi  29760  spanuni  29915  spansneleq  29941  mdi  30666  dmdi  30673  dmdi4  30678  funimass4f  30981  bj-ax89  34868  poimirlem32  35818  ffnafv  44674