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  2855  ovmpox  6160  ovmpoga  6161  nnanq0  7721  apreim  8825  apsub1  8864  divassap  8912  ltmul2  9078  xleadd1  10154  xltadd2  10156  elfzo  10429  fzodcel  10433  subcn2  11934  mulcn2  11935  ndvdsp1  12556  gcddiv  12653  lcmneg  12709  mulgaddcom  13796  lspsnss  14483  rnglidlrng  14577  neipsm  14948  opnneip  14953  hmeof1o2  15102  blcntrps  15209  blcntr  15210  neibl  15285  blnei  15286  metss  15288  rpcxpsub  15702  cxpcom  15732  rplogbzexp  15748  konigsbergssiedgwpren  16409