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  327  intnand  489  intnanrd  490  intn3an1d  1478  intn3an2d  1479  intn3an3d  1480  nsb  2103  necon3ai  2965  pssn2lp  4048  sotrieq  5561  ordnbtwn  6394  funun  6530  canth  7290  0mpo0  7420  dfwe2  7686  opabn1stprc  7966  pwuninel2  8160  frrlem11  8182  frrlem12  8183  swoer  8599  swoord1  8600  swoord2  8601  php2OLD  9088  phpeqdOLD  9090  1sdom2dom  9112  en3lp  9471  cantnfp1lem1  9535  cantnfp1lem3  9537  cantnflem2  9547  rankxpsuc  9739  cardmin2  9856  infxpenlem  9870  cardaleph  9946  isfin4p1  10172  fin23lem24  10179  fin23lem25  10181  fin23lem26  10182  fin23lem38  10206  isfin32i  10222  fin34  10247  fin67  10252  nd3  10446  fpwwe2lem12  10499  canthnum  10506  canthwe  10508  pwfseq  10521  gchdjuidm  10525  gchxpidm  10526  r1wunlim  10594  suplem2pr  10910  elnnz  12430  fzneuz  13438  fzodisj  13522  fzodisjsn  13526  hasheq0  14178  swrd0  14469  cnpart  15050  sqreulem  15170  rlimuni  15358  rlimcld2  15386  divalglem6  16206  bitsf1  16252  infpnlem1  16708  ramubcl  16816  ressress  17055  mreexmrid  17449  gsum2d  19668  dprddomprc  19698  ablfacrplem  19763  trivnsimpgd  19795  ablsimpnosubgd  19802  rng1nfld  20655  mplsubrglem  21316  mdetunilem6  21872  mdetunilem9  21875  madugsum  21898  infil  23120  fbasfip  23125  fgcl  23135  fin1aufil  23189  hauspwpwf1  23244  ovolicc2lem4  24790  ovolioo  24838  i1fima2sn  24950  itg1addlem4  24969  itg1addlem4OLD  24970  itgsplitioo  25108  lhop1lem  25283  chordthmlem  26088  ressatans  26190  ftalem5  26332  ppiprm  26406  chtprm  26408  lgsdir2lem2  26580  dirith2  26782  noresle  26951  noetasuplem4  26990  noetainflem4  26994  axlowdimlem13  27611  axlowdim1  27616  nfrgr2v  28924  inelpisys  32420  eulerpartlemgvv  32643  ballotlemfp1  32758  ballotlem4  32765  ballotlemirc  32798  erdszelem8  33459  bccolsum  33995  nn0prpwlem  34607  nn0prpw  34608  ivthALT  34620  nandsym1  34707  onsucsuccmpi  34728  onint1  34734  bj-fununsn1  35529  bj-fvmptunsn1  35533  topdifinffinlem  35623  relowlssretop  35639  domalom  35680  fin2solem  35868  poimirlem2  35884  poimirlem3  35885  poimirlem4  35886  poimirlem6  35888  poimirlem7  35889  poimirlem8  35890  poimirlem9  35891  poimirlem13  35895  poimirlem14  35896  poimirlem15  35897  poimirlem16  35898  poimirlem17  35899  poimirlem19  35901  poimirlem20  35902  poimirlem21  35903  poimirlem22  35904  poimirlem23  35905  poimirlem26  35908  poimirlem31  35913  mblfinlem1  35919  mblfinlem2  35920  dvasin  35966  dvacos  35967  areacirclem4  35973  ax10fromc7  37162  hdmaplem1  40039  hdmaplem2N  40040  hdmaplem3  40041  negn0nposznnd  40570  irrapx1  40912  gneispace  42065  mnuprdlem2  42212  sineq0ALT  42878  sumnnodd  43507  fperdvper  43796  stoweidlem35  43912  stirlinglem5  43955  fourierdlem68  44051  fourierswlem  44107  fouriersw  44108  iundjiunlem  44334  smfmbfcex  44635  requad1  45425  requad2  45426  zrninitoringc  45980  lmod1zrnlvec  46186  elsetrecslem  46755  et-ltneverrefl  46861  singoutnupword  46869  tworepnotupword  46872