Theorem syl3an3 861

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

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  syl3an3b 864  syl3an3br 867  syl3anl3 875  oprabval4g 4031  unxpdomlem 4843  addsubasst 5383  subcan2t 5402  subcant 5412  subsub4t 5464  pnncant 5480  lesub1t 5660  ltsub1t 5662  ltmul2t 5831  ltdiv2t 5887  uzwo3lem1 6216  faclbnd5 6953  serzmulc1 7057  climge0 7112  iserzmulc1 7136  climcmplem 7137  climsqueeze 7140  climsqueeze2 7141  caucvglem4 7160  caucvglem5 7161  isummulc1ALT 7213  neips 7727  opnneip 7733  lmss 7953  bcthlem1 7999  minveclem26 8570  minveclem27 8571  hvaddsub12t 8907  hvaddsubasst 8910  hvsubdistr1t 8916  hvsubcant 8941  hhssnv 9134  homco1t 9727  homulasst 9728  hoadddirt 9730  hosubdit 9734  hoaddsubasst 9741  hosubsub4t 9744  homco2t 9901  lnopm 9925  adjlnopt 10019  mdsymlem5 10334  hmphsyma 10528

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 777

Copyright terms: Public domain