Theorem nsyli 141

Description: A negated syllogism inference. (Contributed by NM, 3-May-1994.)

Hypotheses

Ref	Expression
nsyli.1
nsyli.2

Assertion

Ref	Expression
nsyli

Proof of Theorem nsyli

Step	Hyp	Ref	Expression
1		nsyli.2	. 2
2		nsyli.1	. . 3
3	2	con3d 133	. 2
4	1, 3	syl5 32	1

Syntax hints:  -.wn 3  ->wi 4

This theorem is referenced by:  necon3ad  2667  tz7.7  4909  tz7.48-2  7126  tz7.49  7129  php  7721  nndomo  7731  elirrv  8044  setind  8186  zorn2lem3  8899  alephval2  8968  inar1  9174  dfon2lem6  29220  sltres  29424  onint1  29914  finminlem  30136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8