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 207  df-an 396

This theorem is referenced by:  ax8  2119  ax9  2127  spcimgft  3503  rspc2  3585  rspc2v  3587  rspc3v  3592  rspc4v  3596  rspc8v  3598  copsexgw  5438  copsexg  5439  chfnrn  6994  fvcofneq  7038  ffnfv  7064  f1elima  7209  onint  7735  peano5  7835  f1oweALT  7916  smoel2  8295  pssnn  9093  php  9131  fiint  9227  dffi2  9326  alephnbtwn  9981  cfcof  10184  zorn2lem7  10412  suplem1pr  10963  addsrpr  10986  mulsrpr  10987  cau3lem  15278  divalglem8  16327  efgi  19648  elfrlmbasn0  21718  locfincmp  23470  tx1stc  23594  fbunfip  23813  filuni  23829  ufileu  23863  rescncf  24846  shmodsi  31464  spanuni  31619  spansneleq  31645  mdi  32370  dmdi  32377  dmdi4  32382  funimass4f  32715  tz9.1regs  35290  bj-ax89  36879  poimirlem32  37853  ffnafv  47417