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  1511  intn3an2d  1512  intn3an3d  1513  nsb  2145  necon3ai  2984  pssn2lp  4035  sotrieq  5595  ordnbtwn  6479  funun  6609  canth  7400  0mpo0  7529  dfwe2  7815  opabn1stprc  8097  pwuninel2  8322  frrlem11  8345  frrlem12  8346  swoer  8780  swoord1  8781  swoord2  8782  1sdom2dom  9276  en3lp  9645  cantnfp1lem1  9709  cantnfp1lem3  9711  cantnflem2  9721  rankxpsuc  9929  cardmin2  10110  infxpenlem  10122  cardaleph  10198  isfin4p1  10423  fin23lem24  10430  fin23lem25  10432  fin23lem26  10433  fin23lem38  10457  isfin32i  10473  fin34  10498  fin67  10503  nd3  10704  fpwwe2lem12  10757  canthnum  10764  canthwe  10766  pwfseq  10779  gchdjuidm  10783  gchxpidm  10784  r1wunlim  10852  suplem2pr  11168  elnnz  12733  fzneuz  13772  fzodisj  13858  fzodisjsn  13862  hasheq0  14537  swrd0  14839  cnpart  15439  sqreulem  15559  rlimuni  15749  rlimcld2  15777  divalglem6  16600  bitsf1  16648  infpnlem1  17120  ramubcl  17228  ressress  17457  mreexmrid  17849  gsum2d  20219  dprddomprc  20249  ablfacrplem  20314  trivnsimpgd  20346  ablsimpnosubgd  20353  zrninitoringc  20961  rng1nfld  21069  mplsubrglem  22344  mdetunilem6  22965  mdetunilem9  22968  madugsum  22991  infil  24215  fbasfip  24220  fgcl  24230  fin1aufil  24284  hauspwpwf1  24339  ovolicc2lem4  25874  ovolioo  25922  i1fima2sn  26034  itg1addlem4  26053  itgsplitioo  26191  lhop1lem  26366  chordthmlem  27193  ressatans  27295  ftalem5  27437  ppiprm  27511  chtprm  27513  lgsdir2lem2  27686  dirith2  27888  noresle  28087  noetasuplem4  28126  noetainflem4  28130  elnnzs  28820  axlowdimlem13  29565  axlowdim1  29570  nfrgr2v  30906  gsumfs2d  33698  ply1annnr  34418  inelpisys  34870  eulerpartlemgvv  35091  ballotlemfp1  35207  ballotlem4  35214  ballotlemirc  35247  kardval  35933  erdszelem8  36143  bccolsum  36695  nn0prpwlem  37301  nn0prpw  37302  ivthALT  37314  nandsym1  37401  onsucsuccmpi  37422  onint1  37428  weiunpo  37444  bj-fununsn1  38379  bj-fvmptunsn1  38383  topdifinffinlem  38475  relowlssretop  38491  domalom  38532  fin2solem  38734  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem9  38752  poimirlem13  38756  poimirlem14  38757  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem21  38764  poimirlem22  38765  poimirlem23  38766  poimirlem26  38769  poimirlem31  38774  mblfinlem1  38780  mblfinlem2  38781  dvasin  38827  dvacos  38828  areacirclem4  38834  ax10fromc7  40155  hdmaplem1  43031  hdmaplem2N  43032  hdmaplem3  43033  negn0nposznnd  43543  fimgmcyc  43802  irrapx1  44039  limnsuc  44470  gneispace  45337  mnuprdlem2  45460  sineq0ALT  46121  sumnnodd  46857  fperdvper  47144  stoweidlem35  47260  stirlinglem5  47303  fourierdlem68  47399  fourierswlem  47455  fouriersw  47456  iundjiunlem  47684  smfmbfcex  47985  et-ltneverrefl  48096  et-sqrtnegnre  48098  requad1  48935  requad2  48936  lmod1zrnlvec  49821  initopropdlemlem  50576  elsetrecslem  51082