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  2957  pssn2lp  4056  sotrieq  5563  ordnbtwn  6412  funun  6538  canth  7312  0mpo0  7441  dfwe2  7719  opabn1stprc  8002  pwuninel2  8216  frrlem11  8238  frrlem12  8239  swoer  8666  swoord1  8667  swoord2  8668  1sdom2dom  9154  en3lp  9523  cantnfp1lem1  9587  cantnfp1lem3  9589  cantnflem2  9599  rankxpsuc  9794  cardmin2  9911  infxpenlem  9923  cardaleph  9999  isfin4p1  10225  fin23lem24  10232  fin23lem25  10234  fin23lem26  10235  fin23lem38  10259  isfin32i  10275  fin34  10300  fin67  10305  nd3  10500  fpwwe2lem12  10553  canthnum  10560  canthwe  10562  pwfseq  10575  gchdjuidm  10579  gchxpidm  10580  r1wunlim  10648  suplem2pr  10964  elnnz  12498  fzneuz  13524  fzodisj  13609  fzodisjsn  13613  hasheq0  14286  swrd0  14582  cnpart  15163  sqreulem  15283  rlimuni  15473  rlimcld2  15501  divalglem6  16325  bitsf1  16373  infpnlem1  16838  ramubcl  16946  ressress  17174  mreexmrid  17566  gsum2d  19901  dprddomprc  19931  ablfacrplem  19996  trivnsimpgd  20028  ablsimpnosubgd  20035  zrninitoringc  20609  rng1nfld  20712  mplsubrglem  21959  mdetunilem6  22561  mdetunilem9  22564  madugsum  22587  infil  23807  fbasfip  23812  fgcl  23822  fin1aufil  23876  hauspwpwf1  23931  ovolicc2lem4  25477  ovolioo  25525  i1fima2sn  25637  itg1addlem4  25656  itgsplitioo  25795  lhop1lem  25974  chordthmlem  26798  ressatans  26900  ftalem5  27043  ppiprm  27117  chtprm  27119  lgsdir2lem2  27293  dirith2  27495  noresle  27665  noetasuplem4  27704  noetainflem4  27708  elnnzs  28397  axlowdimlem13  29027  axlowdim1  29032  nfrgr2v  30347  gsumfs2d  33144  ply1annnr  33860  inelpisys  34311  eulerpartlemgvv  34533  ballotlemfp1  34649  ballotlem4  34656  ballotlemirc  34689  erdszelem8  35392  bccolsum  35933  nn0prpwlem  36516  nn0prpw  36517  ivthALT  36529  nandsym1  36616  onsucsuccmpi  36637  onint1  36643  weiunpo  36659  bj-fununsn1  37458  bj-fvmptunsn1  37462  topdifinffinlem  37552  relowlssretop  37568  domalom  37609  fin2solem  37807  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem9  37830  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem26  37847  poimirlem31  37852  mblfinlem1  37858  mblfinlem2  37859  dvasin  37905  dvacos  37906  areacirclem4  37912  ax10fromc7  39155  hdmaplem1  42031  hdmaplem2N  42032  hdmaplem3  42033  negn0nposznnd  42537  fimgmcyc  42789  irrapx1  43070  limnsuc  43507  gneispace  44375  mnuprdlem2  44514  sineq0ALT  45177  sumnnodd  45876  fperdvper  46163  stoweidlem35  46279  stirlinglem5  46322  fourierdlem68  46418  fourierswlem  46474  fouriersw  46475  iundjiunlem  46703  smfmbfcex  47004  et-ltneverrefl  47115  et-sqrtnegnre  47117  requad1  47868  requad2  47869  lmod1zrnlvec  48740  initopropdlemlem  49484  elsetrecslem  49944