Theorem syl3an3 860

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 831	. . 3 |- (ph -> (ps -> (ch -> th)))
3		syl3an3.2	. . 3 |- (ta -> ch)
4	2, 3	syl7 23	. 2 |- (ph -> (ps -> (ta -> th)))
5	4	3imp 826	1 |- ((ph /\ ps /\ ta) -> th)

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  syl3an3b 863  syl3an3br 866  syl3anl3 873  oprabval4g 4022  unxpdomlem 4823  addsubasst 5363  subcan2t 5382  subcant 5392  subsub4t 5444  pnncant 5460  lesub1t 5641  ltsub1t 5643  ltmul2t 5795  ltdiv2t 5843  uzwo3lem1 6172  faclbnd5 6898  serzmulc1 7003  climge0 7057  iserzmulc1 7080  climcmplem 7081  climsqueeze 7084  climsqueeze2 7085  caucvglem4 7104  caucvglem5 7105  isummulc1ALT 7156  neips 7677  opnneip 7683  lmss 7904  bcthlem1 7949  minveclem26 8514  minveclem27 8515  hvaddsub12t 8846  hvaddsubasst 8849  hvsubdistr1t 8855  hvsubcant 8880  hhssnv 9073  homco1t 9667  homulasst 9668  hoadddirt 9670  hosubdit 9674  hoaddsubasst 9681  hosubsub4t 9684  homco2t 9840  lnopm 9863  adjlnopt 9957  mdsymlem5 10271  hmphsyma 10451

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 776

Copyright terms: Public domain