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  4058  sotrieq  5571  ordnbtwn  6420  funun  6546  canth  7322  0mpo0  7451  dfwe2  7729  opabn1stprc  8012  pwuninel2  8226  frrlem11  8248  frrlem12  8249  swoer  8677  swoord1  8678  swoord2  8679  1sdom2dom  9166  en3lp  9535  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem2  9611  rankxpsuc  9806  cardmin2  9923  infxpenlem  9935  cardaleph  10011  isfin4p1  10237  fin23lem24  10244  fin23lem25  10246  fin23lem26  10247  fin23lem38  10271  isfin32i  10287  fin34  10312  fin67  10317  nd3  10512  fpwwe2lem12  10565  canthnum  10572  canthwe  10574  pwfseq  10587  gchdjuidm  10591  gchxpidm  10592  r1wunlim  10660  suplem2pr  10976  elnnz  12510  fzneuz  13536  fzodisj  13621  fzodisjsn  13625  hasheq0  14298  swrd0  14594  cnpart  15175  sqreulem  15295  rlimuni  15485  rlimcld2  15513  divalglem6  16337  bitsf1  16385  infpnlem1  16850  ramubcl  16958  ressress  17186  mreexmrid  17578  gsum2d  19913  dprddomprc  19943  ablfacrplem  20008  trivnsimpgd  20040  ablsimpnosubgd  20047  zrninitoringc  20621  rng1nfld  20724  mplsubrglem  21971  mdetunilem6  22573  mdetunilem9  22576  madugsum  22599  infil  23819  fbasfip  23824  fgcl  23834  fin1aufil  23888  hauspwpwf1  23943  ovolicc2lem4  25489  ovolioo  25537  i1fima2sn  25649  itg1addlem4  25668  itgsplitioo  25807  lhop1lem  25986  chordthmlem  26810  ressatans  26912  ftalem5  27055  ppiprm  27129  chtprm  27131  lgsdir2lem2  27305  dirith2  27507  noresle  27677  noetasuplem4  27716  noetainflem4  27720  elnnzs  28409  axlowdimlem13  29039  axlowdim1  29044  nfrgr2v  30359  gsumfs2d  33154  ply1annnr  33880  inelpisys  34331  eulerpartlemgvv  34553  ballotlemfp1  34669  ballotlem4  34676  ballotlemirc  34709  erdszelem8  35411  bccolsum  35952  nn0prpwlem  36535  nn0prpw  36536  ivthALT  36548  nandsym1  36635  onsucsuccmpi  36656  onint1  36662  weiunpo  36678  bj-fununsn1  37505  bj-fvmptunsn1  37509  topdifinffinlem  37599  relowlssretop  37615  domalom  37656  fin2solem  37854  poimirlem2  37870  poimirlem3  37871  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem9  37877  poimirlem13  37881  poimirlem14  37882  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem21  37889  poimirlem22  37890  poimirlem23  37891  poimirlem26  37894  poimirlem31  37899  mblfinlem1  37905  mblfinlem2  37906  dvasin  37952  dvacos  37953  areacirclem4  37959  ax10fromc7  39268  hdmaplem1  42144  hdmaplem2N  42145  hdmaplem3  42146  negn0nposznnd  42649  fimgmcyc  42901  irrapx1  43182  limnsuc  43619  gneispace  44487  mnuprdlem2  44626  sineq0ALT  45289  sumnnodd  45987  fperdvper  46274  stoweidlem35  46390  stirlinglem5  46433  fourierdlem68  46529  fourierswlem  46585  fouriersw  46586  iundjiunlem  46814  smfmbfcex  47115  et-ltneverrefl  47226  et-sqrtnegnre  47228  requad1  47979  requad2  47980  lmod1zrnlvec  48851  initopropdlemlem  49595  elsetrecslem  50055