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  6184  ovmpoga  6185  nnanq0  7775  apreim  8879  apsub1  8918  divassap  8966  ltmul2  9132  xleadd1  10211  xltadd2  10213  elfzo  10487  fzodcel  10491  subcn2  12000  mulcn2  12001  ndvdsp1  12622  gcddiv  12719  lcmneg  12775  mulgaddcom  13880  lspsnss  14569  rnglidlrng  14663  neipsm  15036  opnneip  15041  hmeof1o2  15190  blcntrps  15297  blcntr  15298  neibl  15373  blnei  15374  metss  15376  rpcxpsub  15790  cxpcom  15820  rplogbzexp  15836  konigsbergssiedgwpren  16497