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  8931  apsub1  8970  divassap  9020  ltmul2  9186  ind0  9301  xleadd1  10277  xltadd2  10279  elfzo  10556  fzodcel  10560  subcn2  12077  mulcn2  12078  ndvdsp1  12699  gcddiv  12796  lcmneg  12852  mulgaddcom  13949  lspsnss  14741  rnglidlrng  14835  neipsm  15255  opnneip  15260  hmeof1o2  15409  blcntrps  15516  blcntr  15517  neibl  15592  blnei  15593  metss  15595  rpcxpsub  16010  cxpcom  16040  rplogbzexp  16056  konigsbergssiedgwpren  16726