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

Theorem nsyl3 119
Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
Hypotheses
Ref Expression
nsyl3.1
nsyl3.2
Assertion
Ref Expression
nsyl3

Proof of Theorem nsyl3
StepHypRef Expression
1 nsyl3.2 . 2
2 nsyl3.1 . . 3
32a1i 11 . 2
41, 3mt2d 117 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  con2i  120  nsyl  121  cesare  2402  cesaro  2406  pwnss  4617  reusv2lem2  4654  reldmtpos  6982  tz7.49  7129  omopthlem2  7324  domnsym  7663  sdomirr  7674  infensuc  7715  fofinf1o  7821  elfi2  7894  sucprcregOLD  8047  infdifsn  8094  carden2b  8369  alephsucdom  8481  infdif2  8611  fin4i  8699  bitsf1  14096  pcmpt2  14412  ufinffr  20430  chtub  23487  eupath2lem1  24977  gxnval  25262  oddpwdc  28293  eldmgm  28564  lgamucov  28580  facgam  28608  erdszelem10  28644  heiborlem1  30307  fphpd  30750  usgedgnlp  32410  0nodd  32498  bnj1312  34114  osumcllem4N  35683  pexmidlem1N  35694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator