Theorem nsyl 142

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 140	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 141	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  157  sylnib  331  intnand  492  intnanrd  493  intn3an1d  1476  intn3an2d  1477  intn3an3d  1478  pssn2lp  4029  sotrieq  5466  ordnbtwn  6249  funun  6370  canth  7090  0mpo0  7216  dfwe2  7476  opabn1stprc  7738  pwuninel2  7923  swoer  8302  swoord1  8303  swoord2  8304  php2  8686  phpeqd  8690  en3lp  9061  cantnfp1lem1  9125  cantnfp1lem3  9127  cantnflem2  9137  rankxpsuc  9295  cardmin2  9412  infxpenlem  9424  cardaleph  9500  isfin4p1  9726  fin23lem24  9733  fin23lem25  9735  fin23lem26  9736  fin23lem38  9760  isfin32i  9776  fin34  9801  fin67  9806  nd3  10000  fpwwe2lem13  10053  canthnum  10060  canthwe  10062  pwfseq  10075  gchdjuidm  10079  gchxpidm  10080  r1wunlim  10148  suplem2pr  10464  elnnz  11979  fzneuz  12983  fzodisj  13066  fzodisjsn  13070  hasheq0  13720  swrd0  14011  cnpart  14591  sqreulem  14711  rlimuni  14899  rlimcld2  14927  divalglem6  15739  bitsf1  15785  infpnlem1  16236  ramubcl  16344  ressress  16554  mreexmrid  16906  gsum2d  19085  dprddomprc  19115  ablfacrplem  19180  trivnsimpgd  19212  ablsimpnosubgd  19219  rng1nfld  20044  mplsubrglem  20677  mdetunilem6  21222  mdetunilem9  21225  madugsum  21248  infil  22468  fbasfip  22473  fgcl  22483  fin1aufil  22537  hauspwpwf1  22592  ovolicc2lem4  24124  ovolioo  24172  i1fima2sn  24284  itg1addlem4  24303  itgsplitioo  24441  lhop1lem  24616  chordthmlem  25418  ressatans  25520  ftalem5  25662  ppiprm  25736  chtprm  25738  lgsdir2lem2  25910  dirith2  26112  axlowdimlem13  26748  axlowdim1  26753  nfrgr2v  28057  inelpisys  31523  eulerpartlemgvv  31744  ballotlemfp1  31859  ballotlem4  31866  ballotlemirc  31899  erdszelem8  32558  bccolsum  33084  frrlem11  33246  frrlem12  33247  noresle  33313  noetalem3  33332  nn0prpwlem  33783  nn0prpw  33784  ivthALT  33796  nandsym1  33883  onsucsuccmpi  33904  onint1  33910  bj-fununsn1  34668  bj-fvmptunsn1  34672  topdifinffinlem  34764  relowlssretop  34780  domalom  34821  fin2solem  35043  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem26  35083  poimirlem31  35088  mblfinlem1  35094  mblfinlem2  35095  dvasin  35141  dvacos  35142  areacirclem4  35148  ax10fromc7  36191  hdmaplem1  39067  hdmaplem2N  39068  hdmaplem3  39069  negn0nposznnd  39476  irrapx1  39769  gneispace  40837  mnuprdlem2  40981  sineq0ALT  41643  sumnnodd  42272  fperdvper  42561  stoweidlem35  42677  stirlinglem5  42720  fourierdlem68  42816  fourierswlem  42872  fouriersw  42873  iundjiunlem  43098  smfmbfcex  43393  requad1  44140  requad2  44141  zrninitoringc  44695  lmod1zrnlvec  44903  elsetrecslem  45228