Theorem nsyl 141

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 139	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 140	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  155  sylnib  331  intnand  493  intnanrd  494  intn3an1d  1510  intn3an2d  1511  intn3an3d  1512  nsb  2141  necon3ai  2983  pssn2lp  4060  sotrieq  5602  ordnbtwn  6458  funun  6584  canth  7366  0mpo0  7495  dfwe2  7774  opabn1stprc  8056  pwuninel2  8271  frrlem11  8294  frrlem12  8295  swoer  8727  swoord1  8728  swoord2  8729  1sdom2dom  9215  en3lp  9584  cantnfp1lem1  9648  cantnfp1lem3  9650  cantnflem2  9660  rankxpsuc  9855  cardmin2  9986  infxpenlem  9998  cardaleph  10074  isfin4p1  10300  fin23lem24  10307  fin23lem25  10309  fin23lem26  10310  fin23lem38  10334  isfin32i  10350  fin34  10375  fin67  10380  nd3  10575  fpwwe2lem12  10628  canthnum  10635  canthwe  10637  pwfseq  10650  gchdjuidm  10654  gchxpidm  10655  r1wunlim  10723  suplem2pr  11039  elnnz  12602  fzneuz  13638  fzodisj  13724  fzodisjsn  13728  hasheq0  14401  swrd0  14698  cnpart  15293  sqreulem  15413  rlimuni  15603  rlimcld2  15631  divalglem6  16457  bitsf1  16505  infpnlem1  16971  ramubcl  17079  ressress  17308  mreexmrid  17700  gsum2d  20043  dprddomprc  20073  ablfacrplem  20138  trivnsimpgd  20170  ablsimpnosubgd  20177  zrninitoringc  20762  rng1nfld  20863  mplsubrglem  22134  mdetunilem6  22755  mdetunilem9  22758  madugsum  22781  infil  24001  fbasfip  24006  fgcl  24016  fin1aufil  24070  hauspwpwf1  24125  ovolicc2lem4  25660  ovolioo  25708  i1fima2sn  25820  itg1addlem4  25839  itgsplitioo  25978  lhop1lem  26153  chordthmlem  26978  ressatans  27080  ftalem5  27222  ppiprm  27296  chtprm  27298  lgsdir2lem2  27471  dirith2  27673  noresle  27842  noetasuplem4  27881  noetainflem4  27885  elnnzs  28575  axlowdimlem13  29285  axlowdim1  29290  nfrgr2v  30604  gsumfs2d  33362  ply1annnr  34074  inelpisys  34525  eulerpartlemgvv  34747  ballotlemfp1  34863  ballotlem4  34870  ballotlemirc  34903  kardval  35546  erdszelem8  35671  bccolsum  36212  nn0prpwlem  36814  nn0prpw  36815  ivthALT  36827  nandsym1  36914  onsucsuccmpi  36935  onint1  36941  weiunpo  36957  bj-fununsn1  37878  bj-fvmptunsn1  37882  topdifinffinlem  37974  relowlssretop  37990  domalom  38031  fin2solem  38238  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem9  38261  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem23  38275  poimirlem26  38278  poimirlem31  38283  mblfinlem1  38289  mblfinlem2  38290  dvasin  38336  dvacos  38337  areacirclem4  38343  ax10fromc7  39650  hdmaplem1  42526  hdmaplem2N  42527  hdmaplem3  42528  negn0nposznnd  43024  fimgmcyc  43285  irrapx1  43538  limnsuc  43975  gneispace  44843  mnuprdlem2  44966  sineq0ALT  45628  sumnnodd  46329  fperdvper  46616  stoweidlem35  46732  stirlinglem5  46775  fourierdlem68  46871  fourierswlem  46927  fouriersw  46928  iundjiunlem  47156  smfmbfcex  47457  et-ltneverrefl  47568  et-sqrtnegnre  47570  requad1  48370  requad2  48371  lmod1zrnlvec  49257  initopropdlemlem  50000  elsetrecslem  50460