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

Theorem nsyl 140
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 138 . 2 (𝜒 → ¬ 𝜑)
43con2i 139 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  154  sylnib  328  intnand  490  intnanrd  491  intn3an1d  1480  intn3an2d  1481  intn3an3d  1482  nsb  2105  necon3ai  2969  pssn2lp  4066  sotrieq  5579  ordnbtwn  6415  funun  6552  canth  7315  0mpo0  7445  dfwe2  7713  opabn1stprc  7995  pwuninel2  8210  frrlem11  8232  frrlem12  8233  swoer  8685  swoord1  8686  swoord2  8687  php2OLD  9174  phpeqdOLD  9176  1sdom2dom  9198  en3lp  9557  cantnfp1lem1  9621  cantnfp1lem3  9623  cantnflem2  9633  rankxpsuc  9825  cardmin2  9942  infxpenlem  9956  cardaleph  10032  isfin4p1  10258  fin23lem24  10265  fin23lem25  10267  fin23lem26  10268  fin23lem38  10292  isfin32i  10308  fin34  10333  fin67  10338  nd3  10532  fpwwe2lem12  10585  canthnum  10592  canthwe  10594  pwfseq  10607  gchdjuidm  10611  gchxpidm  10612  r1wunlim  10680  suplem2pr  10996  elnnz  12516  fzneuz  13529  fzodisj  13613  fzodisjsn  13617  hasheq0  14270  swrd0  14553  cnpart  15132  sqreulem  15251  rlimuni  15439  rlimcld2  15467  divalglem6  16287  bitsf1  16333  infpnlem1  16789  ramubcl  16897  ressress  17136  mreexmrid  17530  gsum2d  19756  dprddomprc  19786  ablfacrplem  19851  trivnsimpgd  19883  ablsimpnosubgd  19890  rng1nfld  20764  mplsubrglem  21426  mdetunilem6  21982  mdetunilem9  21985  madugsum  22008  infil  23230  fbasfip  23235  fgcl  23245  fin1aufil  23299  hauspwpwf1  23354  ovolicc2lem4  24900  ovolioo  24948  i1fima2sn  25060  itg1addlem4  25079  itg1addlem4OLD  25080  itgsplitioo  25218  lhop1lem  25393  chordthmlem  26198  ressatans  26300  ftalem5  26442  ppiprm  26516  chtprm  26518  lgsdir2lem2  26690  dirith2  26892  noresle  27061  noetasuplem4  27100  noetainflem4  27104  axlowdimlem13  27945  axlowdim1  27950  nfrgr2v  29258  inelpisys  32793  eulerpartlemgvv  33016  ballotlemfp1  33131  ballotlem4  33138  ballotlemirc  33171  erdszelem8  33832  bccolsum  34351  nn0prpwlem  34823  nn0prpw  34824  ivthALT  34836  nandsym1  34923  onsucsuccmpi  34944  onint1  34950  bj-fununsn1  35753  bj-fvmptunsn1  35757  topdifinffinlem  35847  relowlssretop  35863  domalom  35904  fin2solem  36093  poimirlem2  36109  poimirlem3  36110  poimirlem4  36111  poimirlem6  36113  poimirlem7  36114  poimirlem8  36115  poimirlem9  36116  poimirlem13  36120  poimirlem14  36121  poimirlem15  36122  poimirlem16  36123  poimirlem17  36124  poimirlem19  36126  poimirlem20  36127  poimirlem21  36128  poimirlem22  36129  poimirlem23  36130  poimirlem26  36133  poimirlem31  36138  mblfinlem1  36144  mblfinlem2  36145  dvasin  36191  dvacos  36192  areacirclem4  36198  ax10fromc7  37386  hdmaplem1  40263  hdmaplem2N  40264  hdmaplem3  40265  negn0nposznnd  40825  irrapx1  41180  limnsuc  41629  gneispace  42480  mnuprdlem2  42627  sineq0ALT  43293  sumnnodd  43945  fperdvper  44234  stoweidlem35  44350  stirlinglem5  44393  fourierdlem68  44489  fourierswlem  44545  fouriersw  44546  iundjiunlem  44774  smfmbfcex  45075  et-ltneverrefl  45186  et-sqrtnegnre  45188  singoutnupword  45196  tworepnotupword  45199  requad1  45888  requad2  45889  zrninitoringc  46443  lmod1zrnlvec  46649  elsetrecslem  47218
  Copyright terms: Public domain W3C validator