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  330  intnand  492  intnanrd  493  intn3an1d  1499  intn3an2d  1500  intn3an3d  1501  nsb  2139  necon3ai  2981  pssn2lp  4056  sotrieq  5582  ordnbtwn  6435  funun  6561  canth  7344  0mpo0  7473  dfwe2  7751  opabn1stprc  8033  pwuninel2  8247  frrlem11  8270  frrlem12  8271  swoer  8703  swoord1  8704  swoord2  8705  1sdom2dom  9191  en3lp  9562  cantnfp1lem1  9626  cantnfp1lem3  9628  cantnflem2  9638  rankxpsuc  9833  cardmin2  9950  infxpenlem  9962  cardaleph  10038  isfin4p1  10265  fin23lem24  10272  fin23lem25  10274  fin23lem26  10275  fin23lem38  10299  isfin32i  10315  fin34  10340  fin67  10345  nd3  10540  fpwwe2lem12  10593  canthnum  10600  canthwe  10602  pwfseq  10615  gchdjuidm  10619  gchxpidm  10620  r1wunlim  10688  suplem2pr  11004  elnnz  12571  fzneuz  13606  fzodisj  13692  fzodisjsn  13696  hasheq0  14369  swrd0  14665  cnpart  15257  sqreulem  15377  rlimuni  15567  rlimcld2  15595  divalglem6  16422  bitsf1  16470  infpnlem1  16936  ramubcl  17044  ressress  17273  mreexmrid  17665  gsum2d  20002  dprddomprc  20032  ablfacrplem  20097  trivnsimpgd  20129  ablsimpnosubgd  20136  zrninitoringc  20712  rng1nfld  20815  mplsubrglem  22042  mdetunilem6  22664  mdetunilem9  22667  madugsum  22690  infil  23910  fbasfip  23915  fgcl  23925  fin1aufil  23979  hauspwpwf1  24034  ovolicc2lem4  25569  ovolioo  25617  i1fima2sn  25729  itg1addlem4  25748  itgsplitioo  25887  lhop1lem  26062  chordthmlem  26884  ressatans  26986  ftalem5  27128  ppiprm  27202  chtprm  27204  lgsdir2lem2  27377  dirith2  27579  noresle  27748  noetasuplem4  27787  noetainflem4  27791  elnnzs  28481  axlowdimlem13  29111  axlowdim1  29116  nfrgr2v  30430  gsumfs2d  33201  ply1annnr  33960  inelpisys  34411  eulerpartlemgvv  34633  ballotlemfp1  34749  ballotlem4  34756  ballotlemirc  34789  erdszelem8  35508  bccolsum  36049  nn0prpwlem  36642  nn0prpw  36643  ivthALT  36655  nandsym1  36742  onsucsuccmpi  36763  onint1  36769  weiunpo  36785  bj-fununsn1  37705  bj-fvmptunsn1  37709  topdifinffinlem  37801  relowlssretop  37817  domalom  37858  fin2solem  38065  poimirlem2  38081  poimirlem3  38082  poimirlem4  38083  poimirlem6  38085  poimirlem7  38086  poimirlem8  38087  poimirlem9  38088  poimirlem13  38092  poimirlem14  38093  poimirlem15  38094  poimirlem16  38095  poimirlem17  38096  poimirlem19  38098  poimirlem20  38099  poimirlem21  38100  poimirlem22  38101  poimirlem23  38102  poimirlem26  38105  poimirlem31  38110  mblfinlem1  38116  mblfinlem2  38117  dvasin  38163  dvacos  38164  areacirclem4  38170  ax10fromc7  39479  hdmaplem1  42355  hdmaplem2N  42356  hdmaplem3  42357  negn0nposznnd  42851  fimgmcyc  43112  irrapx1  43365  limnsuc  43802  gneispace  44670  mnuprdlem2  44809  sineq0ALT  45472  sumnnodd  46166  fperdvper  46453  stoweidlem35  46569  stirlinglem5  46612  fourierdlem68  46708  fourierswlem  46764  fouriersw  46765  iundjiunlem  46993  smfmbfcex  47294  et-ltneverrefl  47405  et-sqrtnegnre  47407  requad1  48204  requad2  48205  lmod1zrnlvec  49076  initopropdlemlem  49820  elsetrecslem  50280