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 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con3i  155  sylnib  331  intnand  494  intnanrd  495  intn3an1d  1510  intn3an2d  1511  intn3an3d  1512  nsb  2144  necon3ai  2986  pssn2lp  4062  sotrieq  5605  ordnbtwn  6463  funun  6589  canth  7377  0mpo0  7506  dfwe2  7782  opabn1stprc  8064  pwuninel2  8279  frrlem11  8302  frrlem12  8303  swoer  8735  swoord1  8736  swoord2  8737  1sdom2dom  9224  en3lp  9593  cantnfp1lem1  9657  cantnfp1lem3  9659  cantnflem2  9669  rankxpsuc  9864  cardmin2  10004  infxpenlem  10016  cardaleph  10092  isfin4p1  10317  fin23lem24  10324  fin23lem25  10326  fin23lem26  10327  fin23lem38  10351  isfin32i  10367  fin34  10392  fin67  10397  nd3  10592  fpwwe2lem12  10645  canthnum  10652  canthwe  10654  pwfseq  10667  gchdjuidm  10671  gchxpidm  10672  r1wunlim  10740  suplem2pr  11056  elnnz  12619  fzneuz  13655  fzodisj  13741  fzodisjsn  13745  hasheq0  14419  swrd0  14720  cnpart  15317  sqreulem  15437  rlimuni  15627  rlimcld2  15655  divalglem6  16481  bitsf1  16529  infpnlem1  16995  ramubcl  17103  ressress  17332  mreexmrid  17724  gsum2d  20073  dprddomprc  20103  ablfacrplem  20168  trivnsimpgd  20200  ablsimpnosubgd  20207  zrninitoringc  20812  rng1nfld  20919  mplsubrglem  22190  mdetunilem6  22811  mdetunilem9  22814  madugsum  22837  infil  24057  fbasfip  24062  fgcl  24072  fin1aufil  24126  hauspwpwf1  24181  ovolicc2lem4  25716  ovolioo  25764  i1fima2sn  25876  itg1addlem4  25895  itgsplitioo  26034  lhop1lem  26209  chordthmlem  27034  ressatans  27136  ftalem5  27278  ppiprm  27352  chtprm  27354  lgsdir2lem2  27527  dirith2  27729  noresle  27898  noetasuplem4  27937  noetainflem4  27941  elnnzs  28631  axlowdimlem13  29341  axlowdim1  29346  nfrgr2v  30660  gsumfs2d  33412  ply1annnr  34124  inelpisys  34576  eulerpartlemgvv  34798  ballotlemfp1  34914  ballotlem4  34921  ballotlemirc  34954  kardval  35589  erdszelem8  35711  bccolsum  36252  nn0prpwlem  36874  nn0prpw  36875  ivthALT  36887  nandsym1  36974  onsucsuccmpi  36995  onint1  37001  weiunpo  37017  bj-fununsn1  37938  bj-fvmptunsn1  37942  topdifinffinlem  38034  relowlssretop  38050  domalom  38091  fin2solem  38298  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem9  38321  poimirlem13  38325  poimirlem14  38326  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem23  38335  poimirlem26  38338  poimirlem31  38343  mblfinlem1  38349  mblfinlem2  38350  dvasin  38396  dvacos  38397  areacirclem4  38403  ax10fromc7  39710  hdmaplem1  42586  hdmaplem2N  42587  hdmaplem3  42588  negn0nposznnd  43084  fimgmcyc  43343  irrapx1  43596  limnsuc  44033  gneispace  44901  mnuprdlem2  45024  sineq0ALT  45686  sumnnodd  46387  fperdvper  46674  stoweidlem35  46790  stirlinglem5  46833  fourierdlem68  46929  fourierswlem  46985  fouriersw  46986  iundjiunlem  47214  smfmbfcex  47515  et-ltneverrefl  47626  et-sqrtnegnre  47628  requad1  48428  requad2  48429  lmod1zrnlvec  49315  initopropdlemlem  50058  elsetrecslem  50518