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  2958  pssn2lp  4045  sotrieq  5563  ordnbtwn  6412  funun  6538  canth  7314  0mpo0  7443  dfwe2  7721  opabn1stprc  8004  pwuninel2  8217  frrlem11  8239  frrlem12  8240  swoer  8668  swoord1  8669  swoord2  8670  1sdom2dom  9157  en3lp  9526  cantnfp1lem1  9590  cantnfp1lem3  9592  cantnflem2  9602  rankxpsuc  9797  cardmin2  9914  infxpenlem  9926  cardaleph  10002  isfin4p1  10228  fin23lem24  10235  fin23lem25  10237  fin23lem26  10238  fin23lem38  10262  isfin32i  10278  fin34  10303  fin67  10308  nd3  10503  fpwwe2lem12  10556  canthnum  10563  canthwe  10565  pwfseq  10578  gchdjuidm  10582  gchxpidm  10583  r1wunlim  10651  suplem2pr  10967  elnnz  12525  fzneuz  13553  fzodisj  13639  fzodisjsn  13643  hasheq0  14316  swrd0  14612  cnpart  15193  sqreulem  15313  rlimuni  15503  rlimcld2  15531  divalglem6  16358  bitsf1  16406  infpnlem1  16872  ramubcl  16980  ressress  17208  mreexmrid  17600  gsum2d  19938  dprddomprc  19968  ablfacrplem  20033  trivnsimpgd  20065  ablsimpnosubgd  20072  zrninitoringc  20644  rng1nfld  20747  mplsubrglem  21992  mdetunilem6  22592  mdetunilem9  22595  madugsum  22618  infil  23838  fbasfip  23843  fgcl  23853  fin1aufil  23907  hauspwpwf1  23962  ovolicc2lem4  25497  ovolioo  25545  i1fima2sn  25657  itg1addlem4  25676  itgsplitioo  25815  lhop1lem  25990  chordthmlem  26809  ressatans  26911  ftalem5  27054  ppiprm  27128  chtprm  27130  lgsdir2lem2  27303  dirith2  27505  noresle  27675  noetasuplem4  27714  noetainflem4  27718  elnnzs  28407  axlowdimlem13  29037  axlowdim1  29042  nfrgr2v  30357  gsumfs2d  33137  ply1annnr  33863  inelpisys  34314  eulerpartlemgvv  34536  ballotlemfp1  34652  ballotlem4  34659  ballotlemirc  34692  erdszelem8  35396  bccolsum  35937  nn0prpwlem  36520  nn0prpw  36521  ivthALT  36533  nandsym1  36620  onsucsuccmpi  36641  onint1  36647  weiunpo  36663  bj-fununsn1  37583  bj-fvmptunsn1  37587  topdifinffinlem  37677  relowlssretop  37693  domalom  37734  fin2solem  37941  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem9  37964  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem26  37981  poimirlem31  37986  mblfinlem1  37992  mblfinlem2  37993  dvasin  38039  dvacos  38040  areacirclem4  38046  ax10fromc7  39355  hdmaplem1  42231  hdmaplem2N  42232  hdmaplem3  42233  negn0nposznnd  42728  fimgmcyc  42993  irrapx1  43274  limnsuc  43711  gneispace  44579  mnuprdlem2  44718  sineq0ALT  45381  sumnnodd  46078  fperdvper  46365  stoweidlem35  46481  stirlinglem5  46524  fourierdlem68  46620  fourierswlem  46676  fouriersw  46677  iundjiunlem  46905  smfmbfcex  47206  et-ltneverrefl  47317  et-sqrtnegnre  47319  requad1  48110  requad2  48111  lmod1zrnlvec  48982  initopropdlemlem  49726  elsetrecslem  50186