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  1481  intn3an2d  1482  intn3an3d  1483  nsb  2111  necon3ai  2954  pssn2lp  4053  sotrieq  5560  ordnbtwn  6408  funun  6534  canth  7308  0mpo0  7437  dfwe2  7715  opabn1stprc  7998  pwuninel2  8212  frrlem11  8234  frrlem12  8235  swoer  8661  swoord1  8662  swoord2  8663  1sdom2dom  9147  en3lp  9513  cantnfp1lem1  9577  cantnfp1lem3  9579  cantnflem2  9589  rankxpsuc  9784  cardmin2  9901  infxpenlem  9913  cardaleph  9989  isfin4p1  10215  fin23lem24  10222  fin23lem25  10224  fin23lem26  10225  fin23lem38  10249  isfin32i  10265  fin34  10290  fin67  10295  nd3  10489  fpwwe2lem12  10542  canthnum  10549  canthwe  10551  pwfseq  10564  gchdjuidm  10568  gchxpidm  10569  r1wunlim  10637  suplem2pr  10953  elnnz  12487  fzneuz  13512  fzodisj  13597  fzodisjsn  13601  hasheq0  14274  swrd0  14570  cnpart  15151  sqreulem  15271  rlimuni  15461  rlimcld2  15489  divalglem6  16313  bitsf1  16361  infpnlem1  16826  ramubcl  16934  ressress  17162  mreexmrid  17553  gsum2d  19888  dprddomprc  19918  ablfacrplem  19983  trivnsimpgd  20015  ablsimpnosubgd  20022  zrninitoringc  20595  rng1nfld  20698  mplsubrglem  21944  mdetunilem6  22535  mdetunilem9  22538  madugsum  22561  infil  23781  fbasfip  23786  fgcl  23796  fin1aufil  23850  hauspwpwf1  23905  ovolicc2lem4  25451  ovolioo  25499  i1fima2sn  25611  itg1addlem4  25630  itgsplitioo  25769  lhop1lem  25948  chordthmlem  26772  ressatans  26874  ftalem5  27017  ppiprm  27091  chtprm  27093  lgsdir2lem2  27267  dirith2  27469  noresle  27639  noetasuplem4  27678  noetainflem4  27682  elnnzs  28328  axlowdimlem13  28936  axlowdim1  28941  nfrgr2v  30256  gsumfs2d  33044  ply1annnr  33739  inelpisys  34190  eulerpartlemgvv  34412  ballotlemfp1  34528  ballotlem4  34535  ballotlemirc  34568  erdszelem8  35265  bccolsum  35806  nn0prpwlem  36389  nn0prpw  36390  ivthALT  36402  nandsym1  36489  onsucsuccmpi  36510  onint1  36516  weiunpo  36532  bj-fununsn1  37320  bj-fvmptunsn1  37324  topdifinffinlem  37414  relowlssretop  37430  domalom  37471  fin2solem  37669  poimirlem2  37685  poimirlem3  37686  poimirlem4  37687  poimirlem6  37689  poimirlem7  37690  poimirlem8  37691  poimirlem9  37692  poimirlem13  37696  poimirlem14  37697  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem19  37702  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem23  37706  poimirlem26  37709  poimirlem31  37714  mblfinlem1  37720  mblfinlem2  37721  dvasin  37767  dvacos  37768  areacirclem4  37774  ax10fromc7  39017  hdmaplem1  41893  hdmaplem2N  41894  hdmaplem3  41895  negn0nposznnd  42403  fimgmcyc  42655  irrapx1  42948  limnsuc  43385  gneispace  44254  mnuprdlem2  44393  sineq0ALT  45056  sumnnodd  45757  fperdvper  46044  stoweidlem35  46160  stirlinglem5  46203  fourierdlem68  46299  fourierswlem  46355  fouriersw  46356  iundjiunlem  46584  smfmbfcex  46885  et-ltneverrefl  46996  et-sqrtnegnre  46998  requad1  47749  requad2  47750  lmod1zrnlvec  48622  initopropdlemlem  49367  elsetrecslem  49827