Theorem syl3an3 1285

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  syl3an3b  1288  syl3an3br  1291  vtoclgft  2823  ovmpox  6074  ovmpoga  6075  nnanq0  7571  apreim  8676  apsub1  8715  divassap  8763  ltmul2  8929  xleadd1  9997  xltadd2  9999  elfzo  10271  fzodcel  10275  subcn2  11622  mulcn2  11623  ndvdsp1  12243  gcddiv  12340  lcmneg  12396  mulgaddcom  13482  lspsnss  14166  rnglidlrng  14260  neipsm  14626  opnneip  14631  hmeof1o2  14780  blcntrps  14887  blcntr  14888  neibl  14963  blnei  14964  metss  14966  rpcxpsub  15380  cxpcom  15410  rplogbzexp  15426