Theorem syl3an3 1306

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem syl3an3

Step	Hyp	Ref	Expression
1		syl3an3.1	. . 3 |- ( ph -> th )
2		syl3an3.2	. . . 4 |- ( ( ps /\ ch /\ th ) -> ta )
3	2	3exp 1226	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl7 69	. 2 |- ( ps -> ( ch -> ( ph -> ta ) ) )
5	4	3imp 1217	1 |- ( ( ps /\ ch /\ ph ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  syl3an3b  1309  syl3an3br  1312  vtoclgft  2851  ovmpox  6132  ovmpoga  6133  nnanq0  7641  apreim  8746  apsub1  8785  divassap  8833  ltmul2  8999  xleadd1  10067  xltadd2  10069  elfzo  10341  fzodcel  10345  subcn2  11817  mulcn2  11818  ndvdsp1  12438  gcddiv  12535  lcmneg  12591  mulgaddcom  13678  lspsnss  14362  rnglidlrng  14456  neipsm  14822  opnneip  14827  hmeof1o2  14976  blcntrps  15083  blcntr  15084  neibl  15159  blnei  15160  metss  15162  rpcxpsub  15576  cxpcom  15606  rplogbzexp  15622