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  329  intnand  489  intnanrd  490  intn3an1d  1487  intn3an2d  1488  intn3an3d  1489  nsb  2117  necon3ai  2960  pssn2lp  4042  sotrieq  5564  ordnbtwn  6412  funun  6538  canth  7317  0mpo0  7446  dfwe2  7724  opabn1stprc  8007  pwuninel2  8221  frrlem11  8243  frrlem12  8244  swoer  8672  swoord1  8673  swoord2  8674  1sdom2dom  9161  en3lp  9533  cantnfp1lem1  9597  cantnfp1lem3  9599  cantnflem2  9609  rankxpsuc  9804  cardmin2  9921  infxpenlem  9933  cardaleph  10009  isfin4p1  10235  fin23lem24  10242  fin23lem25  10244  fin23lem26  10245  fin23lem38  10269  isfin32i  10285  fin34  10310  fin67  10315  nd3  10510  fpwwe2lem12  10563  canthnum  10570  canthwe  10572  pwfseq  10585  gchdjuidm  10589  gchxpidm  10590  r1wunlim  10658  suplem2pr  10974  elnnz  12532  fzneuz  13560  fzodisj  13646  fzodisjsn  13650  hasheq0  14323  swrd0  14619  cnpart  15200  sqreulem  15320  rlimuni  15510  rlimcld2  15538  divalglem6  16365  bitsf1  16413  infpnlem1  16879  ramubcl  16987  ressress  17215  mreexmrid  17607  gsum2d  19945  dprddomprc  19975  ablfacrplem  20040  trivnsimpgd  20072  ablsimpnosubgd  20079  zrninitoringc  20655  rng1nfld  20758  mplsubrglem  21985  mdetunilem6  22607  mdetunilem9  22610  madugsum  22633  infil  23853  fbasfip  23858  fgcl  23868  fin1aufil  23922  hauspwpwf1  23977  ovolicc2lem4  25512  ovolioo  25560  i1fima2sn  25672  itg1addlem4  25691  itgsplitioo  25830  lhop1lem  26005  chordthmlem  26821  ressatans  26923  ftalem5  27065  ppiprm  27139  chtprm  27141  lgsdir2lem2  27314  dirith2  27516  noresle  27686  noetasuplem4  27725  noetainflem4  27729  elnnzs  28418  axlowdimlem13  29048  axlowdim1  29053  nfrgr2v  30367  gsumfs2d  33149  ply1annnr  33894  inelpisys  34345  eulerpartlemgvv  34567  ballotlemfp1  34683  ballotlem4  34690  ballotlemirc  34723  erdszelem8  35433  bccolsum  35974  nn0prpwlem  36557  nn0prpw  36558  ivthALT  36570  nandsym1  36657  onsucsuccmpi  36678  onint1  36684  weiunpo  36700  bj-fununsn1  37620  bj-fvmptunsn1  37624  topdifinffinlem  37716  relowlssretop  37732  domalom  37773  fin2solem  37980  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem9  38003  poimirlem13  38007  poimirlem14  38008  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem26  38020  poimirlem31  38025  mblfinlem1  38031  mblfinlem2  38032  dvasin  38078  dvacos  38079  areacirclem4  38085  ax10fromc7  39394  hdmaplem1  42270  hdmaplem2N  42271  hdmaplem3  42272  negn0nposznnd  42766  fimgmcyc  43027  irrapx1  43280  limnsuc  43717  gneispace  44585  mnuprdlem2  44724  sineq0ALT  45387  sumnnodd  46082  fperdvper  46369  stoweidlem35  46485  stirlinglem5  46528  fourierdlem68  46624  fourierswlem  46680  fouriersw  46681  iundjiunlem  46909  smfmbfcex  47210  et-ltneverrefl  47321  et-sqrtnegnre  47323  requad1  48120  requad2  48121  lmod1zrnlvec  48992  initopropdlemlem  49736  elsetrecslem  50196