Theorem syl3an3 1284

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  syl3an3b  1287  syl3an3br  1290  vtoclgft  2814  ovmpox  6055  ovmpoga  6056  nnanq0  7542  apreim  8647  apsub1  8686  divassap  8734  ltmul2  8900  xleadd1  9967  xltadd2  9969  elfzo  10241  fzodcel  10245  subcn2  11493  mulcn2  11494  ndvdsp1  12114  gcddiv  12211  lcmneg  12267  mulgaddcom  13352  lspsnss  14036  rnglidlrng  14130  neipsm  14474  opnneip  14479  hmeof1o2  14628  blcntrps  14735  blcntr  14736  neibl  14811  blnei  14812  metss  14814  rpcxpsub  15228  cxpcom  15258  rplogbzexp  15274