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  2814  ovmpox  6055  ovmpoga  6056  nnanq0  7544  apreim  8649  apsub1  8688  divassap  8736  ltmul2  8902  xleadd1  9969  xltadd2  9971  elfzo  10243  fzodcel  10247  subcn2  11495  mulcn2  11496  ndvdsp1  12116  gcddiv  12213  lcmneg  12269  mulgaddcom  13354  lspsnss  14038  rnglidlrng  14132  neipsm  14476  opnneip  14481  hmeof1o2  14630  blcntrps  14737  blcntr  14738  neibl  14813  blnei  14814  metss  14816  rpcxpsub  15230  cxpcom  15260  rplogbzexp  15276