Theorem syl3an3 1209

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

Syntax hints:   -> wi 4   /\ w3a 924

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

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  syl3an3b  1212  syl3an3br  1215  vtoclgft  2669  ovmpt2x  5773  ovmpt2ga  5774  nnanq0  7015  apreim  8078  apsub1  8115  divassap  8155  ltmul2  8315  elfzo  9556  fzodcel  9559  subcn2  10696  mulcn2  10697  ndvdsp1  11206  gcddiv  11282  lcmneg  11330