Theorem syl3an3 1283

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

Syntax hints:   -> wi 4   /\ w3a 979

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 981

This theorem is referenced by:  syl3an3b  1286  syl3an3br  1289  vtoclgft  2799  ovmpox  6017  ovmpoga  6018  nnanq0  7471  apreim  8574  apsub1  8613  divassap  8661  ltmul2  8827  xleadd1  9889  xltadd2  9891  elfzo  10163  fzodcel  10166  subcn2  11333  mulcn2  11334  ndvdsp1  11951  gcddiv  12034  lcmneg  12088  mulgaddcom  13047  lspsnss  13650  rnglidlrng  13744  neipsm  14007  opnneip  14012  hmeof1o2  14161  blcntrps  14268  blcntr  14269  neibl  14344  blnei  14345  metss  14347  rpcxpsub  14682  cxpcom  14710  rplogbzexp  14725