MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyli Unicode version

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
StepHypRef Expression
1 nsyli.2 . 2
2 nsyli.1 . . 3
32con3d 133 . 2
41, 3syl5 32 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator