Theorem syl3an3 1309

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  syl3an3b  1312  syl3an3br  1315  vtoclgft  2865  ovmpox  6182  ovmpoga  6183  nnanq0  7773  apreim  8877  apsub1  8916  divassap  8964  ltmul2  9130  xleadd1  10208  xltadd2  10210  elfzo  10483  fzodcel  10487  subcn2  11996  mulcn2  11997  ndvdsp1  12618  gcddiv  12715  lcmneg  12771  mulgaddcom  13863  lspsnss  14552  rnglidlrng  14646  neipsm  15019  opnneip  15024  hmeof1o2  15173  blcntrps  15280  blcntr  15281  neibl  15356  blnei  15357  metss  15359  rpcxpsub  15773  cxpcom  15803  rplogbzexp  15819  konigsbergssiedgwpren  16480