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  2982  pssn2lp  4056  sotrieq  5598  ordnbtwn  6457  funun  6583  canth  7371  0mpo0  7500  dfwe2  7777  opabn1stprc  8059  pwuninel2  8276  frrlem11  8299  frrlem12  8300  swoer  8732  swoord1  8733  swoord2  8734  1sdom2dom  9228  en3lp  9597  cantnfp1lem1  9661  cantnfp1lem3  9663  cantnflem2  9673  rankxpsuc  9868  cardmin2  10008  infxpenlem  10020  cardaleph  10096  isfin4p1  10321  fin23lem24  10328  fin23lem25  10330  fin23lem26  10331  fin23lem38  10355  isfin32i  10371  fin34  10396  fin67  10401  nd3  10602  fpwwe2lem12  10655  canthnum  10662  canthwe  10664  pwfseq  10677  gchdjuidm  10681  gchxpidm  10682  r1wunlim  10750  suplem2pr  11066  elnnz  12629  fzneuz  13667  fzodisj  13753  fzodisjsn  13757  hasheq0  14431  swrd0  14732  cnpart  15331  sqreulem  15451  rlimuni  15641  rlimcld2  15669  divalglem6  16494  bitsf1  16542  infpnlem1  17008  ramubcl  17116  ressress  17345  mreexmrid  17737  gsum2d  20105  dprddomprc  20135  ablfacrplem  20200  trivnsimpgd  20232  ablsimpnosubgd  20239  zrninitoringc  20844  rng1nfld  20951  mplsubrglem  22224  mdetunilem6  22845  mdetunilem9  22848  madugsum  22871  infil  24095  fbasfip  24100  fgcl  24110  fin1aufil  24164  hauspwpwf1  24219  ovolicc2lem4  25754  ovolioo  25802  i1fima2sn  25914  itg1addlem4  25933  itgsplitioo  26072  lhop1lem  26247  chordthmlem  27077  ressatans  27179  ftalem5  27321  ppiprm  27395  chtprm  27397  lgsdir2lem2  27570  dirith2  27772  noresle  27941  noetasuplem4  27980  noetainflem4  27984  elnnzs  28674  axlowdimlem13  29419  axlowdim1  29424  nfrgr2v  30760  gsumfs2d  33509  ply1annnr  34221  inelpisys  34673  eulerpartlemgvv  34895  ballotlemfp1  35011  ballotlem4  35018  ballotlemirc  35051  kardval  35686  erdszelem8  35785  bccolsum  36326  nn0prpwlem  36949  nn0prpw  36950  ivthALT  36962  nandsym1  37049  onsucsuccmpi  37070  onint1  37076  weiunpo  37092  bj-fununsn1  38013  bj-fvmptunsn1  38017  topdifinffinlem  38109  relowlssretop  38125  domalom  38166  fin2solem  38368  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem13  38390  poimirlem14  38391  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem26  38403  poimirlem31  38408  mblfinlem1  38414  mblfinlem2  38415  dvasin  38461  dvacos  38462  areacirclem4  38468  ax10fromc7  39776  hdmaplem1  42652  hdmaplem2N  42653  hdmaplem3  42654  negn0nposznnd  43165  fimgmcyc  43424  irrapx1  43677  limnsuc  44114  gneispace  44982  mnuprdlem2  45105  sineq0ALT  45767  sumnnodd  46468  fperdvper  46755  stoweidlem35  46871  stirlinglem5  46914  fourierdlem68  47010  fourierswlem  47066  fouriersw  47067  iundjiunlem  47295  smfmbfcex  47596  et-ltneverrefl  47707  et-sqrtnegnre  47709  requad1  48546  requad2  48547  lmod1zrnlvec  49432  initopropdlemlem  50173  elsetrecslem  50633