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  1478  intn3an2d  1479  intn3an3d  1480  nsb  2104  necon3ai  2963  pssn2lp  4114  sotrieq  5627  ordnbtwn  6479  funun  6614  canth  7385  0mpo0  7516  dfwe2  7793  opabn1stprc  8082  pwuninel2  8298  frrlem11  8320  frrlem12  8321  swoer  8775  swoord1  8776  swoord2  8777  php2OLD  9258  phpeqdOLD  9260  1sdom2dom  9281  en3lp  9652  cantnfp1lem1  9716  cantnfp1lem3  9718  cantnflem2  9728  rankxpsuc  9920  cardmin2  10037  infxpenlem  10051  cardaleph  10127  isfin4p1  10353  fin23lem24  10360  fin23lem25  10362  fin23lem26  10363  fin23lem38  10387  isfin32i  10403  fin34  10428  fin67  10433  nd3  10627  fpwwe2lem12  10680  canthnum  10687  canthwe  10689  pwfseq  10702  gchdjuidm  10706  gchxpidm  10707  r1wunlim  10775  suplem2pr  11091  elnnz  12621  fzneuz  13645  fzodisj  13730  fzodisjsn  13734  hasheq0  14399  swrd0  14693  cnpart  15276  sqreulem  15395  rlimuni  15583  rlimcld2  15611  divalglem6  16432  bitsf1  16480  infpnlem1  16944  ramubcl  17052  ressress  17294  mreexmrid  17688  gsum2d  20005  dprddomprc  20035  ablfacrplem  20100  trivnsimpgd  20132  ablsimpnosubgd  20139  zrninitoringc  20693  rng1nfld  20797  mplsubrglem  22042  mdetunilem6  22639  mdetunilem9  22642  madugsum  22665  infil  23887  fbasfip  23892  fgcl  23902  fin1aufil  23956  hauspwpwf1  24011  ovolicc2lem4  25569  ovolioo  25617  i1fima2sn  25729  itg1addlem4  25748  itg1addlem4OLD  25749  itgsplitioo  25888  lhop1lem  26067  chordthmlem  26890  ressatans  26992  ftalem5  27135  ppiprm  27209  chtprm  27211  lgsdir2lem2  27385  dirith2  27587  noresle  27757  noetasuplem4  27796  noetainflem4  27800  elnnzs  28402  axlowdimlem13  28984  axlowdim1  28989  nfrgr2v  30301  gsumfs2d  33041  ply1annnr  33711  inelpisys  34135  eulerpartlemgvv  34358  ballotlemfp1  34473  ballotlem4  34480  ballotlemirc  34513  erdszelem8  35183  bccolsum  35719  nn0prpwlem  36305  nn0prpw  36306  ivthALT  36318  nandsym1  36405  onsucsuccmpi  36426  onint1  36432  weiunpo  36448  bj-fununsn1  37236  bj-fvmptunsn1  37240  topdifinffinlem  37330  relowlssretop  37346  domalom  37387  fin2solem  37593  poimirlem2  37609  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem9  37616  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem23  37630  poimirlem26  37633  poimirlem31  37638  mblfinlem1  37644  mblfinlem2  37645  dvasin  37691  dvacos  37692  areacirclem4  37698  ax10fromc7  38877  hdmaplem1  41754  hdmaplem2N  41755  hdmaplem3  41756  negn0nposznnd  42296  fimgmcyc  42521  irrapx1  42816  limnsuc  43255  gneispace  44124  mnuprdlem2  44269  sineq0ALT  44935  sumnnodd  45586  fperdvper  45875  stoweidlem35  45991  stirlinglem5  46034  fourierdlem68  46130  fourierswlem  46186  fouriersw  46187  iundjiunlem  46415  smfmbfcex  46716  et-ltneverrefl  46827  et-sqrtnegnre  46829  singoutnupword  46837  tworepnotupword  46840  requad1  47547  requad2  47548  lmod1zrnlvec  48340  elsetrecslem  48930