Theorem syl3an3 1285

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  syl3an3b  1288  syl3an3br  1291  vtoclgft  2828  ovmpox  6097  ovmpoga  6098  nnanq0  7606  apreim  8711  apsub1  8750  divassap  8798  ltmul2  8964  xleadd1  10032  xltadd2  10034  elfzo  10306  fzodcel  10310  subcn2  11737  mulcn2  11738  ndvdsp1  12358  gcddiv  12455  lcmneg  12511  mulgaddcom  13597  lspsnss  14281  rnglidlrng  14375  neipsm  14741  opnneip  14746  hmeof1o2  14895  blcntrps  15002  blcntr  15003  neibl  15078  blnei  15079  metss  15081  rpcxpsub  15495  cxpcom  15525  rplogbzexp  15541