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  7826  apreim  8934  apsub1  8973  divassap  9023  ltmul2  9189  ind0  9304  xleadd1  10288  xltadd2  10290  elfzo  10567  fzodcel  10571  subcn2  12096  mulcn2  12097  ndvdsp1  12718  gcddiv  12815  lcmneg  12871  mulgaddcom  14002  lspsnss  14825  rnglidlrng  14919  neipsm  15346  opnneip  15351  hmeof1o2  15500  blcntrps  15607  blcntr  15608  neibl  15683  blnei  15684  metss  15686  rpcxpsub  16105  cxpcom  16135  rplogbzexp  16151  konigsbergssiedgwpren  16892