Theorem sylan9 517

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 78	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	imp 412	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ax8  2151  ax9  2159  spcimgft  3510  rspc2  3585  rspc2v  3587  rspc3v  3592  rspc4v  3596  rspc8v  3598  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  chfnrn  7041  fvcofneq  7086  ffnfv  7112  f1elima  7260  onint  7789  peano5  7890  f1oweALT  7969  smoel2  8352  pssnn  9163  php  9201  fiint  9296  dffi2  9393  alephnbtwn  10074  cfcof  10276  zorn2lem7  10504  suplem1pr  11061  addsrpr  11084  mulsrpr  11085  cau3lem  15442  divalglem8  16490  efgi  19846  elfrlmbasn0  21976  locfincmp  23752  tx1stc  23876  fbunfip  24095  filuni  24111  ufileu  24145  rescncf  25125  shmodsi  31870  spanuni  32025  spansneleq  32051  mdi  32776  dmdi  32783  dmdi4  32788  funimass4f  33110  tz9.1regs  35660  bj-ax89  37409  poimirlem32  38401  ffnafv  48059