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

Step	Hyp	Ref	Expression
1		nsyl.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		nsyl.2	. . 3 ⊢ (𝜒 → 𝜓)
3	1, 2	nsyl3 138	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 139	1 ⊢ (𝜑 → ¬ 𝜒)

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  488  intnanrd  489  intn3an1d  1482  intn3an2d  1483  intn3an3d  1484  nsb  2112  necon3ai  2957  pssn2lp  4044  sotrieq  5570  ordnbtwn  6418  funun  6544  canth  7321  0mpo0  7450  dfwe2  7728  opabn1stprc  8011  pwuninel2  8224  frrlem11  8246  frrlem12  8247  swoer  8675  swoord1  8676  swoord2  8677  1sdom2dom  9164  en3lp  9535  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem2  9611  rankxpsuc  9806  cardmin2  9923  infxpenlem  9935  cardaleph  10011  isfin4p1  10237  fin23lem24  10244  fin23lem25  10246  fin23lem26  10247  fin23lem38  10271  isfin32i  10287  fin34  10312  fin67  10317  nd3  10512  fpwwe2lem12  10565  canthnum  10572  canthwe  10574  pwfseq  10587  gchdjuidm  10591  gchxpidm  10592  r1wunlim  10660  suplem2pr  10976  elnnz  12534  fzneuz  13562  fzodisj  13648  fzodisjsn  13652  hasheq0  14325  swrd0  14621  cnpart  15202  sqreulem  15322  rlimuni  15512  rlimcld2  15540  divalglem6  16367  bitsf1  16415  infpnlem1  16881  ramubcl  16989  ressress  17217  mreexmrid  17609  gsum2d  19947  dprddomprc  19977  ablfacrplem  20042  trivnsimpgd  20074  ablsimpnosubgd  20081  zrninitoringc  20653  rng1nfld  20756  mplsubrglem  21982  mdetunilem6  22582  mdetunilem9  22585  madugsum  22608  infil  23828  fbasfip  23833  fgcl  23843  fin1aufil  23897  hauspwpwf1  23952  ovolicc2lem4  25487  ovolioo  25535  i1fima2sn  25647  itg1addlem4  25666  itgsplitioo  25805  lhop1lem  25980  chordthmlem  26796  ressatans  26898  ftalem5  27040  ppiprm  27114  chtprm  27116  lgsdir2lem2  27289  dirith2  27491  noresle  27661  noetasuplem4  27700  noetainflem4  27704  elnnzs  28393  axlowdimlem13  29023  axlowdim1  29028  nfrgr2v  30342  gsumfs2d  33122  ply1annnr  33847  inelpisys  34298  eulerpartlemgvv  34520  ballotlemfp1  34636  ballotlem4  34643  ballotlemirc  34676  erdszelem8  35380  bccolsum  35921  nn0prpwlem  36504  nn0prpw  36505  ivthALT  36517  nandsym1  36604  onsucsuccmpi  36625  onint1  36631  weiunpo  36647  bj-fununsn1  37567  bj-fvmptunsn1  37571  topdifinffinlem  37663  relowlssretop  37679  domalom  37720  fin2solem  37927  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem26  37967  poimirlem31  37972  mblfinlem1  37978  mblfinlem2  37979  dvasin  38025  dvacos  38026  areacirclem4  38032  ax10fromc7  39341  hdmaplem1  42217  hdmaplem2N  42218  hdmaplem3  42219  negn0nposznnd  42714  fimgmcyc  42979  irrapx1  43256  limnsuc  43693  gneispace  44561  mnuprdlem2  44700  sineq0ALT  45363  sumnnodd  46060  fperdvper  46347  stoweidlem35  46463  stirlinglem5  46506  fourierdlem68  46602  fourierswlem  46658  fouriersw  46659  iundjiunlem  46887  smfmbfcex  47188  et-ltneverrefl  47299  et-sqrtnegnre  47301  requad1  48098  requad2  48099  lmod1zrnlvec  48970  initopropdlemlem  49714  elsetrecslem  50174