MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyl Structured version   Visualization version   GIF version

Theorem nsyl 135
Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Hypotheses
Ref Expression
nsyl.1 (𝜑 → ¬ 𝜓)
nsyl.2 (𝜒𝜓)
Assertion
Ref Expression
nsyl (𝜑 → ¬ 𝜒)

Proof of Theorem nsyl
StepHypRef Expression
1 nsyl.1 . . 3 (𝜑 → ¬ 𝜓)
2 nsyl.2 . . 3 (𝜒𝜓)
31, 2nsyl3 133 . 2 (𝜒 → ¬ 𝜑)
43con2i 134 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  con3i  150  intnand  961  intnanrd  962  intn3an1d  1439  intn3an2d  1440  intn3an3d  1441  camestres  2569  camestros  2573  calemes  2580  calemos  2583  pssn2lp  3686  sotrieq  5022  ordnbtwn  5775  ordnbtwnOLD  5776  funun  5890  canth  6562  dfwe2  6928  opabn1stprc  7173  pwuninel2  7345  swoer  7717  swoord1  7718  swoord2  7719  php2  8089  en3lp  8457  cantnfp1lem1  8519  cantnfp1lem3  8521  cantnflem2  8531  rankxpsuc  8689  cardmin2  8768  infxpenlem  8780  cardaleph  8856  isfin4-3  9081  fin23lem24  9088  fin23lem25  9090  fin23lem26  9091  fin23lem38  9115  isfin32i  9131  fin34  9156  fin67  9161  nd3  9355  fpwwe2lem13  9408  canthnum  9415  canthwe  9417  pwfseq  9430  gchcdaidm  9434  gchxpidm  9435  r1wunlim  9503  suplem2pr  9819  elnnz  11331  fzneuz  12362  fzodisj  12443  fzodisjsn  12446  hasheq0  13094  swrd0  13372  cnpart  13914  sqreulem  14033  rlimuni  14215  rlimcld2  14243  divalglem6  15045  bitsf1  15092  infpnlem1  15538  ramubcl  15646  ressress  15859  mreexmrid  16224  gsum2d  18292  dprddomprc  18320  ablfacrplem  18385  rng1nfld  19197  mplsubrglem  19358  mdetunilem6  20342  mdetunilem9  20345  madugsum  20368  infil  21577  fbasfip  21582  fgcl  21592  fin1aufil  21646  hauspwpwf1  21701  ovolicc2lem4  23195  ovolioo  23243  i1fima2sn  23353  itg1addlem4  23372  itgsplitioo  23510  lhop1lem  23680  chordthmlem  24459  ressatans  24561  ftalem5  24703  ppiprm  24777  chtprm  24779  lgsdir2lem2  24951  dirith2  25117  axlowdimlem13  25734  axlowdim1  25739  nfrgr2v  27000  eulerpartlemgvv  30219  ballotlemfp1  30334  ballotlem4  30341  ballotlemirc  30374  erdszelem8  30888  bccolsum  31333  nodenselem7  31550  nobndup  31563  nobnddown  31564  noreslege  31571  nn0prpwlem  31959  nn0prpw  31960  ivthALT  31972  nandsym1  32063  onsucsuccmpi  32084  onint1  32090  bj-xnex  32701  topdifinffinlem  32827  relowlssretop  32843  fin2solem  33027  poimirlem2  33043  poimirlem3  33044  poimirlem4  33045  poimirlem6  33047  poimirlem7  33048  poimirlem8  33049  poimirlem9  33050  poimirlem13  33054  poimirlem14  33055  poimirlem15  33056  poimirlem16  33057  poimirlem17  33058  poimirlem19  33060  poimirlem20  33061  poimirlem21  33062  poimirlem22  33063  poimirlem23  33064  poimirlem26  33067  poimirlem31  33072  mblfinlem1  33078  mblfinlem2  33079  dvasin  33128  dvacos  33129  areacirclem4  33135  ax10fromc7  33660  hdmaplem1  36540  hdmaplem2N  36541  hdmaplem3  36542  irrapx1  36872  gneispace  37914  sineq0ALT  38656  sumnnodd  39266  fperdvper  39439  stoweidlem35  39559  stirlinglem5  39602  fourierdlem68  39698  fourierswlem  39754  fouriersw  39755  zrninitoringc  41359  lmod1zrnlvec  41571  elsetrecslem  41737
  Copyright terms: Public domain W3C validator