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  6220  ovmpoga  6221  nnanq0  7831  apreim  8939  apsub1  8978  divassap  9028  ltmul2  9194  ind0  9310  xleadd1  10293  xltadd2  10295  elfzo  10572  fzodcel  10576  subcn2  12101  mulcn2  12102  ndvdsp1  12723  gcddiv  12820  lcmneg  12876  mulgaddcom  14007  lspsnss  14849  rnglidlrng  14943  neipsm  15397  opnneip  15402  hmeof1o2  15551  blcntrps  15658  blcntr  15659  neibl  15734  blnei  15735  metss  15737  rpcxpsub  16158  cxpcom  16190  rplogbzexp  16207  konigsbergssiedgwpren  16948