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  2950  pssn2lp  4057  sotrieq  5562  ordnbtwn  6406  funun  6532  canth  7307  0mpo0  7436  dfwe2  7714  opabn1stprc  8000  pwuninel2  8214  frrlem11  8236  frrlem12  8237  swoer  8663  swoord1  8664  swoord2  8665  1sdom2dom  9153  en3lp  9529  cantnfp1lem1  9593  cantnfp1lem3  9595  cantnflem2  9605  rankxpsuc  9797  cardmin2  9914  infxpenlem  9926  cardaleph  10002  isfin4p1  10228  fin23lem24  10235  fin23lem25  10237  fin23lem26  10238  fin23lem38  10262  isfin32i  10278  fin34  10303  fin67  10308  nd3  10502  fpwwe2lem12  10555  canthnum  10562  canthwe  10564  pwfseq  10577  gchdjuidm  10581  gchxpidm  10582  r1wunlim  10650  suplem2pr  10966  elnnz  12499  fzneuz  13529  fzodisj  13614  fzodisjsn  13618  hasheq0  14288  swrd0  14583  cnpart  15165  sqreulem  15285  rlimuni  15475  rlimcld2  15503  divalglem6  16327  bitsf1  16375  infpnlem1  16840  ramubcl  16948  ressress  17176  mreexmrid  17567  gsum2d  19869  dprddomprc  19899  ablfacrplem  19964  trivnsimpgd  19996  ablsimpnosubgd  20003  zrninitoringc  20579  rng1nfld  20682  mplsubrglem  21929  mdetunilem6  22520  mdetunilem9  22523  madugsum  22546  infil  23766  fbasfip  23771  fgcl  23781  fin1aufil  23835  hauspwpwf1  23890  ovolicc2lem4  25437  ovolioo  25485  i1fima2sn  25597  itg1addlem4  25616  itgsplitioo  25755  lhop1lem  25934  chordthmlem  26758  ressatans  26860  ftalem5  27003  ppiprm  27077  chtprm  27079  lgsdir2lem2  27253  dirith2  27455  noresle  27625  noetasuplem4  27664  noetainflem4  27668  elnnzs  28312  axlowdimlem13  28917  axlowdim1  28922  nfrgr2v  30234  gsumfs2d  33021  ply1annnr  33672  inelpisys  34123  eulerpartlemgvv  34346  ballotlemfp1  34462  ballotlem4  34469  ballotlemirc  34502  erdszelem8  35173  bccolsum  35714  nn0prpwlem  36298  nn0prpw  36299  ivthALT  36311  nandsym1  36398  onsucsuccmpi  36419  onint1  36425  weiunpo  36441  bj-fununsn1  37229  bj-fvmptunsn1  37233  topdifinffinlem  37323  relowlssretop  37339  domalom  37380  fin2solem  37588  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem9  37611  poimirlem13  37615  poimirlem14  37616  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem26  37628  poimirlem31  37633  mblfinlem1  37639  mblfinlem2  37640  dvasin  37686  dvacos  37687  areacirclem4  37693  ax10fromc7  38876  hdmaplem1  41753  hdmaplem2N  41754  hdmaplem3  41755  negn0nposznnd  42258  fimgmcyc  42510  irrapx1  42804  limnsuc  43241  gneispace  44110  mnuprdlem2  44249  sineq0ALT  44913  sumnnodd  45615  fperdvper  45904  stoweidlem35  46020  stirlinglem5  46063  fourierdlem68  46159  fourierswlem  46215  fouriersw  46216  iundjiunlem  46444  smfmbfcex  46745  et-ltneverrefl  46856  et-sqrtnegnre  46858  singoutnupword  46868  tworepnotupword  46871  requad1  47610  requad2  47611  lmod1zrnlvec  48483  initopropdlemlem  49228  elsetrecslem  49688