Theorem syl3an3 1273

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  syl3an3b  1276  syl3an3br  1279  vtoclgft  2789  ovmpox  6006  ovmpoga  6007  nnanq0  7460  apreim  8563  apsub1  8602  divassap  8650  ltmul2  8816  xleadd1  9878  xltadd2  9880  elfzo  10152  fzodcel  10155  subcn2  11322  mulcn2  11323  ndvdsp1  11940  gcddiv  12023  lcmneg  12077  mulgaddcom  13013  lspsnss  13496  neipsm  13794  opnneip  13799  hmeof1o2  13948  blcntrps  14055  blcntr  14056  neibl  14131  blnei  14132  metss  14134  rpcxpsub  14469  cxpcom  14497  rplogbzexp  14512