Theorem syl3an3 1306

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  syl3an3b  1309  syl3an3br  1312  vtoclgft  2851  ovmpox  6139  ovmpoga  6140  nnanq0  7656  apreim  8761  apsub1  8800  divassap  8848  ltmul2  9014  xleadd1  10083  xltadd2  10085  elfzo  10357  fzodcel  10361  subcn2  11837  mulcn2  11838  ndvdsp1  12458  gcddiv  12555  lcmneg  12611  mulgaddcom  13698  lspsnss  14383  rnglidlrng  14477  neipsm  14843  opnneip  14848  hmeof1o2  14997  blcntrps  15104  blcntr  15105  neibl  15180  blnei  15181  metss  15183  rpcxpsub  15597  cxpcom  15627  rplogbzexp  15643