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  2811  ovmpox  6048  ovmpoga  6049  nnanq0  7520  apreim  8624  apsub1  8663  divassap  8711  ltmul2  8877  xleadd1  9944  xltadd2  9946  elfzo  10218  fzodcel  10222  subcn2  11457  mulcn2  11458  ndvdsp1  12076  gcddiv  12159  lcmneg  12215  mulgaddcom  13219  lspsnss  13903  rnglidlrng  13997  neipsm  14333  opnneip  14338  hmeof1o2  14487  blcntrps  14594  blcntr  14595  neibl  14670  blnei  14671  metss  14673  rpcxpsub  15084  cxpcom  15112  rplogbzexp  15127