Theorem syl3an3 863

Description: A syllogism inference.

Hypotheses

Ref	Expression
syl3an.1	|- ((ph /\ ps /\ ch) -> th)
syl3an3.2	|- (ta -> ch)

Assertion

Ref	Expression
syl3an3	|- ((ph /\ ps /\ ta) -> th)

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an.1	. . . 4 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 834	. . 3 |- (ph -> (ps -> (ch -> th)))
3		syl3an3.2	. . 3 |- (ta -> ch)
4	2, 3	syl7 23	. 2 |- (ph -> (ps -> (ta -> th)))
5	4	3imp 829	1 |- ((ph /\ ps /\ ta) -> th)

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  syl3an3b 866  syl3an3br 869  syl3anl3 877  oprabval4g 4037  unxpdomlem 4854  addsubasst 5395  subcan2t 5414  subcant 5424  subsub4t 5476  pnncant 5492  lesub1t 5672  ltsub1t 5674  ltmul2t 5833  ltdiv2t 5889  uzwo3lem1 6218  faclbnd5 6953  serzmulc1 7057  climge0 7112  iserzmulc1 7136  climcmplem 7137  climsqueeze 7140  climsqueeze2 7141  caucvglem4 7160  caucvglem5 7161  isummulc1ALT 7213  neips 7724  opnneip 7730  lmss 7950  bcthlem1 7996  minveclem26 8566  minveclem27 8567  hvaddsub12t 8902  hvaddsubasst 8905  hvsubdistr1t 8911  hvsubcant 8936  hhssnv 9129  homco1t 9722  homulasst 9723  hoadddirt 9725  hosubdit 9729  hoaddsubasst 9736  hosubsub4t 9739  homco2t 9896  lnopm 9920  adjlnopt 10014  mdsymlem5 10329  hmphsyma 10514

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain