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  1440  intn3an2d  1441  intn3an3d  1442  camestres  2568  camestros  2572  calemes  2579  calemos  2582  pssn2lp  3700  sotrieq  5052  ordnbtwn  5804  ordnbtwnOLD  5805  funun  5920  canth  6593  dfwe2  6966  opabn1stprc  7213  pwuninel2  7385  swoer  7757  swoord1  7758  swoord2  7759  php2  8130  en3lp  8498  cantnfp1lem1  8560  cantnfp1lem3  8562  cantnflem2  8572  rankxpsuc  8730  cardmin2  8809  infxpenlem  8821  cardaleph  8897  isfin4-3  9122  fin23lem24  9129  fin23lem25  9131  fin23lem26  9132  fin23lem38  9156  isfin32i  9172  fin34  9197  fin67  9202  nd3  9396  fpwwe2lem13  9449  canthnum  9456  canthwe  9458  pwfseq  9471  gchcdaidm  9475  gchxpidm  9476  r1wunlim  9544  suplem2pr  9860  elnnz  11372  fzneuz  12405  fzodisj  12486  fzodisjsn  12489  hasheq0  13137  swrd0  13416  cnpart  13961  sqreulem  14080  rlimuni  14262  rlimcld2  14290  divalglem6  15102  bitsf1  15149  infpnlem1  15595  ramubcl  15703  ressress  15919  mreexmrid  16284  gsum2d  18352  dprddomprc  18380  ablfacrplem  18445  rng1nfld  19259  mplsubrglem  19420  mdetunilem6  20404  mdetunilem9  20407  madugsum  20430  infil  21648  fbasfip  21653  fgcl  21663  fin1aufil  21717  hauspwpwf1  21772  ovolicc2lem4  23269  ovolioo  23317  i1fima2sn  23428  itg1addlem4  23447  itgsplitioo  23585  lhop1lem  23757  chordthmlem  24540  ressatans  24642  ftalem5  24784  ppiprm  24858  chtprm  24860  lgsdir2lem2  25032  dirith2  25198  axlowdimlem13  25815  axlowdim1  25820  nfrgr2v  27116  eulerpartlemgvv  30412  ballotlemfp1  30527  ballotlem4  30534  ballotlemirc  30567  erdszelem8  31154  bccolsum  31600  noresle  31820  noetalem3  31839  nn0prpwlem  32292  nn0prpw  32293  ivthALT  32305  nandsym1  32396  onsucsuccmpi  32417  onint1  32423  topdifinffinlem  33166  relowlssretop  33182  fin2solem  33366  poimirlem2  33382  poimirlem3  33383  poimirlem4  33384  poimirlem6  33386  poimirlem7  33387  poimirlem8  33388  poimirlem9  33389  poimirlem13  33393  poimirlem14  33394  poimirlem15  33395  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem21  33401  poimirlem22  33402  poimirlem23  33403  poimirlem26  33406  poimirlem31  33411  mblfinlem1  33417  mblfinlem2  33418  dvasin  33467  dvacos  33468  areacirclem4  33474  ax10fromc7  33999  hdmaplem1  36879  hdmaplem2N  36880  hdmaplem3  36881  irrapx1  37211  gneispace  38252  sineq0ALT  38993  sumnnodd  39662  fperdvper  39896  stoweidlem35  40015  stirlinglem5  40058  fourierdlem68  40154  fourierswlem  40210  fouriersw  40211  zrninitoringc  41836  lmod1zrnlvec  42048  elsetrecslem  42209
  Copyright terms: Public domain W3C validator