Theorem syl3an3 1313

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 1233	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
4	1, 3	syl7 69	. 2 |- ( ps -> ( ch -> ( ph -> ta ) ) )
5	4	3imp 1224	1 |- ( ( ps /\ ch /\ ph ) -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl3an3b  1316  syl3an3br  1319  vtoclgft  2873  ovmpox  6217  ovmpoga  6218  nnanq0  7825  apreim  8933  apsub1  8972  divassap  9022  ltmul2  9188  ind0  9303  xleadd1  10287  xltadd2  10289  elfzo  10566  fzodcel  10570  subcn2  12093  mulcn2  12094  ndvdsp1  12715  gcddiv  12812  lcmneg  12868  mulgaddcom  13998  lspsnss  14790  rnglidlrng  14884  neipsm  15304  opnneip  15309  hmeof1o2  15458  blcntrps  15565  blcntr  15566  neibl  15641  blnei  15642  metss  15644  rpcxpsub  16063  cxpcom  16093  rplogbzexp  16109  konigsbergssiedgwpren  16824