Theorem syl3an3 1263

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

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  syl3an3b  1266  syl3an3br  1269  vtoclgft  2776  ovmpox  5970  ovmpoga  5971  nnanq0  7399  apreim  8501  apsub1  8540  divassap  8586  ltmul2  8751  xleadd1  9811  xltadd2  9813  elfzo  10084  fzodcel  10087  subcn2  11252  mulcn2  11253  ndvdsp1  11869  gcddiv  11952  lcmneg  12006  neipsm  12804  opnneip  12809  hmeof1o2  12958  blcntrps  13065  blcntr  13066  neibl  13141  blnei  13142  metss  13144  rpcxpsub  13479  cxpcom  13507  rplogbzexp  13522