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  2106  necon3ai  2965  pssn2lp  4104  sotrieq  5623  ordnbtwn  6477  funun  6612  canth  7385  0mpo0  7516  dfwe2  7794  opabn1stprc  8083  pwuninel2  8299  frrlem11  8321  frrlem12  8322  swoer  8776  swoord1  8777  swoord2  8778  php2OLD  9260  phpeqdOLD  9262  1sdom2dom  9283  en3lp  9654  cantnfp1lem1  9718  cantnfp1lem3  9720  cantnflem2  9730  rankxpsuc  9922  cardmin2  10039  infxpenlem  10053  cardaleph  10129  isfin4p1  10355  fin23lem24  10362  fin23lem25  10364  fin23lem26  10365  fin23lem38  10389  isfin32i  10405  fin34  10430  fin67  10435  nd3  10629  fpwwe2lem12  10682  canthnum  10689  canthwe  10691  pwfseq  10704  gchdjuidm  10708  gchxpidm  10709  r1wunlim  10777  suplem2pr  11093  elnnz  12623  fzneuz  13648  fzodisj  13733  fzodisjsn  13737  hasheq0  14402  swrd0  14696  cnpart  15279  sqreulem  15398  rlimuni  15586  rlimcld2  15614  divalglem6  16435  bitsf1  16483  infpnlem1  16948  ramubcl  17056  ressress  17293  mreexmrid  17686  gsum2d  19990  dprddomprc  20020  ablfacrplem  20085  trivnsimpgd  20117  ablsimpnosubgd  20124  zrninitoringc  20676  rng1nfld  20780  mplsubrglem  22024  mdetunilem6  22623  mdetunilem9  22626  madugsum  22649  infil  23871  fbasfip  23876  fgcl  23886  fin1aufil  23940  hauspwpwf1  23995  ovolicc2lem4  25555  ovolioo  25603  i1fima2sn  25715  itg1addlem4  25734  itgsplitioo  25873  lhop1lem  26052  chordthmlem  26875  ressatans  26977  ftalem5  27120  ppiprm  27194  chtprm  27196  lgsdir2lem2  27370  dirith2  27572  noresle  27742  noetasuplem4  27781  noetainflem4  27785  elnnzs  28387  axlowdimlem13  28969  axlowdim1  28974  nfrgr2v  30291  gsumfs2d  33058  ply1annnr  33746  inelpisys  34155  eulerpartlemgvv  34378  ballotlemfp1  34494  ballotlem4  34501  ballotlemirc  34534  erdszelem8  35203  bccolsum  35739  nn0prpwlem  36323  nn0prpw  36324  ivthALT  36336  nandsym1  36423  onsucsuccmpi  36444  onint1  36450  weiunpo  36466  bj-fununsn1  37254  bj-fvmptunsn1  37258  topdifinffinlem  37348  relowlssretop  37364  domalom  37405  fin2solem  37613  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem26  37653  poimirlem31  37658  mblfinlem1  37664  mblfinlem2  37665  dvasin  37711  dvacos  37712  areacirclem4  37718  ax10fromc7  38896  hdmaplem1  41773  hdmaplem2N  41774  hdmaplem3  41775  negn0nposznnd  42317  fimgmcyc  42544  irrapx1  42839  limnsuc  43278  gneispace  44147  mnuprdlem2  44292  sineq0ALT  44957  sumnnodd  45645  fperdvper  45934  stoweidlem35  46050  stirlinglem5  46093  fourierdlem68  46189  fourierswlem  46245  fouriersw  46246  iundjiunlem  46474  smfmbfcex  46775  et-ltneverrefl  46886  et-sqrtnegnre  46888  singoutnupword  46898  tworepnotupword  46901  requad1  47609  requad2  47610  lmod1zrnlvec  48411  elsetrecslem  49218