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  2107  necon3ai  2958  pssn2lp  4084  sotrieq  5597  ordnbtwn  6452  funun  6587  canth  7364  0mpo0  7495  dfwe2  7773  opabn1stprc  8062  pwuninel2  8278  frrlem11  8300  frrlem12  8301  swoer  8755  swoord1  8756  swoord2  8757  php2OLD  9237  phpeqdOLD  9239  1sdom2dom  9260  en3lp  9633  cantnfp1lem1  9697  cantnfp1lem3  9699  cantnflem2  9709  rankxpsuc  9901  cardmin2  10018  infxpenlem  10032  cardaleph  10108  isfin4p1  10334  fin23lem24  10341  fin23lem25  10343  fin23lem26  10344  fin23lem38  10368  isfin32i  10384  fin34  10409  fin67  10414  nd3  10608  fpwwe2lem12  10661  canthnum  10668  canthwe  10670  pwfseq  10683  gchdjuidm  10687  gchxpidm  10688  r1wunlim  10756  suplem2pr  11072  elnnz  12603  fzneuz  13630  fzodisj  13715  fzodisjsn  13719  hasheq0  14386  swrd0  14681  cnpart  15264  sqreulem  15383  rlimuni  15571  rlimcld2  15599  divalglem6  16422  bitsf1  16470  infpnlem1  16935  ramubcl  17043  ressress  17273  mreexmrid  17660  gsum2d  19958  dprddomprc  19988  ablfacrplem  20053  trivnsimpgd  20085  ablsimpnosubgd  20092  zrninitoringc  20641  rng1nfld  20744  mplsubrglem  21969  mdetunilem6  22560  mdetunilem9  22563  madugsum  22586  infil  23806  fbasfip  23811  fgcl  23821  fin1aufil  23875  hauspwpwf1  23930  ovolicc2lem4  25478  ovolioo  25526  i1fima2sn  25638  itg1addlem4  25657  itgsplitioo  25796  lhop1lem  25975  chordthmlem  26799  ressatans  26901  ftalem5  27044  ppiprm  27118  chtprm  27120  lgsdir2lem2  27294  dirith2  27496  noresle  27666  noetasuplem4  27705  noetainflem4  27709  elnnzs  28346  axlowdimlem13  28938  axlowdim1  28943  nfrgr2v  30258  gsumfs2d  33054  ply1annnr  33742  inelpisys  34190  eulerpartlemgvv  34413  ballotlemfp1  34529  ballotlem4  34536  ballotlemirc  34569  erdszelem8  35225  bccolsum  35761  nn0prpwlem  36345  nn0prpw  36346  ivthALT  36358  nandsym1  36445  onsucsuccmpi  36466  onint1  36472  weiunpo  36488  bj-fununsn1  37276  bj-fvmptunsn1  37280  topdifinffinlem  37370  relowlssretop  37386  domalom  37427  fin2solem  37635  poimirlem2  37651  poimirlem3  37652  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem9  37658  poimirlem13  37662  poimirlem14  37663  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem21  37670  poimirlem22  37671  poimirlem23  37672  poimirlem26  37675  poimirlem31  37680  mblfinlem1  37686  mblfinlem2  37687  dvasin  37733  dvacos  37734  areacirclem4  37740  ax10fromc7  38918  hdmaplem1  41795  hdmaplem2N  41796  hdmaplem3  41797  negn0nposznnd  42299  fimgmcyc  42524  irrapx1  42818  limnsuc  43256  gneispace  44125  mnuprdlem2  44264  sineq0ALT  44928  sumnnodd  45626  fperdvper  45915  stoweidlem35  46031  stirlinglem5  46074  fourierdlem68  46170  fourierswlem  46226  fouriersw  46227  iundjiunlem  46455  smfmbfcex  46756  et-ltneverrefl  46867  et-sqrtnegnre  46869  singoutnupword  46879  tworepnotupword  46882  requad1  47603  requad2  47604  lmod1zrnlvec  48437  initopropdlemlem  49123  elsetrecslem  49530