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  2867  ovmpox  6190  ovmpoga  6191  nnanq0  7789  apreim  8894  apsub1  8933  divassap  8981  ltmul2  9147  xleadd1  10227  xltadd2  10229  elfzo  10505  fzodcel  10509  subcn2  12021  mulcn2  12022  ndvdsp1  12643  gcddiv  12740  lcmneg  12796  mulgaddcom  13899  lspsnss  14678  rnglidlrng  14772  neipsm  15145  opnneip  15150  hmeof1o2  15299  blcntrps  15406  blcntr  15407  neibl  15482  blnei  15483  metss  15485  rpcxpsub  15899  cxpcom  15929  rplogbzexp  15945  konigsbergssiedgwpren  16606