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  2143  necon3ai  2981  pssn2lp  4053  sotrieq  5590  ordnbtwn  6451  funun  6578  canth  7366  0mpo0  7495  dfwe2  7777  opabn1stprc  8058  pwuninel2  8275  frrlem11  8298  frrlem12  8299  swoer  8733  swoord1  8734  swoord2  8735  1sdom2dom  9229  en3lp  9599  cantnfp1lem1  9663  cantnfp1lem3  9665  cantnflem2  9675  rankxpsuc  9880  cardmin2  10061  infxpenlem  10073  cardaleph  10149  isfin4p1  10374  fin23lem24  10381  fin23lem25  10383  fin23lem26  10384  fin23lem38  10408  isfin32i  10424  fin34  10449  fin67  10454  nd3  10655  fpwwe2lem12  10708  canthnum  10715  canthwe  10717  pwfseq  10730  gchdjuidm  10734  gchxpidm  10735  r1wunlim  10803  suplem2pr  11119  elnnz  12684  fzneuz  13722  fzodisj  13808  fzodisjsn  13812  hasheq0  14487  swrd0  14788  cnpart  15387  sqreulem  15507  rlimuni  15697  rlimcld2  15725  divalglem6  16548  bitsf1  16596  infpnlem1  17068  ramubcl  17176  ressress  17405  mreexmrid  17797  gsum2d  20166  dprddomprc  20196  ablfacrplem  20261  trivnsimpgd  20293  ablsimpnosubgd  20300  zrninitoringc  20908  rng1nfld  21016  mplsubrglem  22291  mdetunilem6  22912  mdetunilem9  22915  madugsum  22938  infil  24162  fbasfip  24167  fgcl  24177  fin1aufil  24231  hauspwpwf1  24286  ovolicc2lem4  25821  ovolioo  25869  i1fima2sn  25981  itg1addlem4  26000  itgsplitioo  26138  lhop1lem  26313  chordthmlem  27142  ressatans  27244  ftalem5  27386  ppiprm  27460  chtprm  27462  lgsdir2lem2  27635  dirith2  27837  noresle  28036  noetasuplem4  28075  noetainflem4  28079  elnnzs  28769  axlowdimlem13  29514  axlowdim1  29519  nfrgr2v  30855  gsumfs2d  33604  ply1annnr  34317  inelpisys  34769  eulerpartlemgvv  34991  ballotlemfp1  35107  ballotlem4  35114  ballotlemirc  35147  kardval  35793  erdszelem8  35932  bccolsum  36473  nn0prpwlem  37080  nn0prpw  37081  ivthALT  37093  nandsym1  37180  onsucsuccmpi  37201  onint1  37207  weiunpo  37223  bj-fununsn1  38142  bj-fvmptunsn1  38146  topdifinffinlem  38238  relowlssretop  38254  domalom  38295  fin2solem  38497  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem9  38515  poimirlem13  38519  poimirlem14  38520  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem26  38532  poimirlem31  38537  mblfinlem1  38543  mblfinlem2  38544  dvasin  38590  dvacos  38591  areacirclem4  38597  ax10fromc7  39920  hdmaplem1  42796  hdmaplem2N  42797  hdmaplem3  42798  negn0nposznnd  43307  fimgmcyc  43560  irrapx1  43788  limnsuc  44225  gneispace  45093  mnuprdlem2  45216  sineq0ALT  45878  sumnnodd  46586  fperdvper  46873  stoweidlem35  46989  stirlinglem5  47032  fourierdlem68  47128  fourierswlem  47184  fouriersw  47185  iundjiunlem  47413  smfmbfcex  47714  et-ltneverrefl  47825  et-sqrtnegnre  47827  requad1  48664  requad2  48665  lmod1zrnlvec  49550  initopropdlemlem  50291  elsetrecslem  50736