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  2107  necon3ai  2950  pssn2lp  4067  sotrieq  5577  ordnbtwn  6427  funun  6562  canth  7341  0mpo0  7472  dfwe2  7750  opabn1stprc  8037  pwuninel2  8253  frrlem11  8275  frrlem12  8276  swoer  8702  swoord1  8703  swoord2  8704  1sdom2dom  9194  en3lp  9567  cantnfp1lem1  9631  cantnfp1lem3  9633  cantnflem2  9643  rankxpsuc  9835  cardmin2  9952  infxpenlem  9966  cardaleph  10042  isfin4p1  10268  fin23lem24  10275  fin23lem25  10277  fin23lem26  10278  fin23lem38  10302  isfin32i  10318  fin34  10343  fin67  10348  nd3  10542  fpwwe2lem12  10595  canthnum  10602  canthwe  10604  pwfseq  10617  gchdjuidm  10621  gchxpidm  10622  r1wunlim  10690  suplem2pr  11006  elnnz  12539  fzneuz  13569  fzodisj  13654  fzodisjsn  13658  hasheq0  14328  swrd0  14623  cnpart  15206  sqreulem  15326  rlimuni  15516  rlimcld2  15544  divalglem6  16368  bitsf1  16416  infpnlem1  16881  ramubcl  16989  ressress  17217  mreexmrid  17604  gsum2d  19902  dprddomprc  19932  ablfacrplem  19997  trivnsimpgd  20029  ablsimpnosubgd  20036  zrninitoringc  20585  rng1nfld  20688  mplsubrglem  21913  mdetunilem6  22504  mdetunilem9  22507  madugsum  22530  infil  23750  fbasfip  23755  fgcl  23765  fin1aufil  23819  hauspwpwf1  23874  ovolicc2lem4  25421  ovolioo  25469  i1fima2sn  25581  itg1addlem4  25600  itgsplitioo  25739  lhop1lem  25918  chordthmlem  26742  ressatans  26844  ftalem5  26987  ppiprm  27061  chtprm  27063  lgsdir2lem2  27237  dirith2  27439  noresle  27609  noetasuplem4  27648  noetainflem4  27652  elnnzs  28289  axlowdimlem13  28881  axlowdim1  28886  nfrgr2v  30201  gsumfs2d  32995  ply1annnr  33693  inelpisys  34144  eulerpartlemgvv  34367  ballotlemfp1  34483  ballotlem4  34490  ballotlemirc  34523  erdszelem8  35185  bccolsum  35726  nn0prpwlem  36310  nn0prpw  36311  ivthALT  36323  nandsym1  36410  onsucsuccmpi  36431  onint1  36437  weiunpo  36453  bj-fununsn1  37241  bj-fvmptunsn1  37245  topdifinffinlem  37335  relowlssretop  37351  domalom  37392  fin2solem  37600  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem26  37640  poimirlem31  37645  mblfinlem1  37651  mblfinlem2  37652  dvasin  37698  dvacos  37699  areacirclem4  37705  ax10fromc7  38888  hdmaplem1  41765  hdmaplem2N  41766  hdmaplem3  41767  negn0nposznnd  42270  fimgmcyc  42522  irrapx1  42816  limnsuc  43254  gneispace  44123  mnuprdlem2  44262  sineq0ALT  44926  sumnnodd  45628  fperdvper  45917  stoweidlem35  46033  stirlinglem5  46076  fourierdlem68  46172  fourierswlem  46228  fouriersw  46229  iundjiunlem  46457  smfmbfcex  46758  et-ltneverrefl  46869  et-sqrtnegnre  46871  singoutnupword  46881  tworepnotupword  46884  requad1  47620  requad2  47621  lmod1zrnlvec  48480  initopropdlemlem  49225  elsetrecslem  49685