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

Theorem nsyl2 127
 Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.)
Hypotheses
Ref Expression
nsyl2.1
nsyl2.2
Assertion
Ref Expression
nsyl2

Proof of Theorem nsyl2
StepHypRef Expression
1 nsyl2.1 . 2
2 nsyl2.2 . . 3
32a1i 11 . 2
41, 3mt3d 125 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4 This theorem is referenced by:  con1i  129  con4i  130  oprcl  4242  ovrcl  6329  tfi  6688  limom  6715  oaabs2  7313  ecexr  7335  elpmi  7457  elmapex  7459  pmresg  7466  pmsspw  7473  ixpssmap2g  7518  ixpssmapg  7519  resixpfo  7527  infensuc  7715  pm54.43lem  8401  alephnbtwn  8473  cfpwsdom  8980  elbasfv  14679  elbasov  14680  restsspw  14829  homarcl  15355  isipodrs  15791  grpidval  15887  efgrelexlema  16767  subcmn  16845  dvdsrval  17294  mvrf1  18081  pf1rcl  18385  elocv  18699  matrcl  18914  restrcl  19658  ssrest  19677  iscnp2  19740  isfcls  20510  isnghm  21230  dchrrcl  23515  eleenn  24199  hmdmadj  26859  indispcon  28679  cvmtop1  28705  cvmtop2  28706  mrsub0  28876  mrsubf  28877  mrsubccat  28878  mrsubcn  28879  mrsubco  28881  mrsubvrs  28882  msubf  28892  mclsrcl  28921  dfon2lem7  29221  sltval2  29416  sltres  29424  funpartlem  29592  rankeq1o  29828  mapco2g  30646  atbase  35014  llnbase  35233  lplnbase  35258  lvolbase  35302  lhpbase  35722 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
 Copyright terms: Public domain W3C validator