Theorem syl3an3 1268

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

Syntax hints:   -> wi 4   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  syl3an3b  1271  syl3an3br  1274  vtoclgft  2780  ovmpox  5981  ovmpoga  5982  nnanq0  7420  apreim  8522  apsub1  8561  divassap  8607  ltmul2  8772  xleadd1  9832  xltadd2  9834  elfzo  10105  fzodcel  10108  subcn2  11274  mulcn2  11275  ndvdsp1  11891  gcddiv  11974  lcmneg  12028  neipsm  12948  opnneip  12953  hmeof1o2  13102  blcntrps  13209  blcntr  13210  neibl  13285  blnei  13286  metss  13288  rpcxpsub  13623  cxpcom  13651  rplogbzexp  13666