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  2117  ax9  2125  spcimgft  3499  rspc2  3581  rspc2v  3583  rspc3v  3588  rspc4v  3592  rspc8v  3594  copsexgw  5433  copsexg  5434  chfnrn  6988  fvcofneq  7032  ffnfv  7058  f1elima  7203  onint  7729  peano5  7829  f1oweALT  7910  smoel2  8289  pssnn  9084  php  9122  fiint  9217  dffi2  9313  alephnbtwn  9968  cfcof  10171  zorn2lem7  10399  suplem1pr  10949  addsrpr  10972  mulsrpr  10973  cau3lem  15268  divalglem8  16317  efgi  19637  elfrlmbasn0  21706  locfincmp  23447  tx1stc  23571  fbunfip  23790  filuni  23806  ufileu  23840  rescncf  24823  shmodsi  31376  spanuni  31531  spansneleq  31557  mdi  32282  dmdi  32289  dmdi4  32294  funimass4f  32626  tz9.1regs  35137  bj-ax89  36729  poimirlem32  37698  ffnafv  47276