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  2142  necon3ai  2980  pssn2lp  4032  sotrieq  5589  ordnbtwn  6458  funun  6586  canth  7374  0mpo0  7503  dfwe2  7788  opabn1stprc  8069  pwuninel2  8294  frrlem11  8317  frrlem12  8318  swoer  8752  swoord1  8753  swoord2  8754  1sdom2dom  9248  en3lp  9618  cantnfp1lem1  9682  cantnfp1lem3  9684  cantnflem2  9694  rankxpsuc  9902  cardmin2  10083  infxpenlem  10095  cardaleph  10171  isfin4p1  10396  fin23lem24  10403  fin23lem25  10405  fin23lem26  10406  fin23lem38  10430  isfin32i  10446  fin34  10471  fin67  10476  nd3  10677  fpwwe2lem12  10730  canthnum  10737  canthwe  10739  pwfseq  10752  gchdjuidm  10756  gchxpidm  10757  r1wunlim  10825  suplem2pr  11141  elnnz  12706  fzneuz  13745  fzodisj  13831  fzodisjsn  13835  hasheq0  14510  swrd0  14812  cnpart  15412  sqreulem  15532  rlimuni  15722  rlimcld2  15750  divalglem6  16573  bitsf1  16621  infpnlem1  17093  ramubcl  17201  ressress  17430  mreexmrid  17822  gsum2d  20191  dprddomprc  20221  ablfacrplem  20286  trivnsimpgd  20318  ablsimpnosubgd  20325  zrninitoringc  20933  rng1nfld  21041  mplsubrglem  22316  mdetunilem6  22937  mdetunilem9  22940  madugsum  22963  infil  24187  fbasfip  24192  fgcl  24202  fin1aufil  24256  hauspwpwf1  24311  ovolicc2lem4  25846  ovolioo  25894  i1fima2sn  26006  itg1addlem4  26025  itgsplitioo  26163  lhop1lem  26338  chordthmlem  27165  ressatans  27267  ftalem5  27409  ppiprm  27483  chtprm  27485  lgsdir2lem2  27658  dirith2  27860  noresle  28059  noetasuplem4  28098  noetainflem4  28102  elnnzs  28792  axlowdimlem13  29537  axlowdim1  29542  nfrgr2v  30878  gsumfs2d  33668  ply1annnr  34381  inelpisys  34833  eulerpartlemgvv  35054  ballotlemfp1  35170  ballotlem4  35177  ballotlemirc  35210  kardval  35876  erdszelem8  36049  bccolsum  36596  nn0prpwlem  37202  nn0prpw  37203  ivthALT  37215  nandsym1  37302  onsucsuccmpi  37323  onint1  37329  weiunpo  37345  bj-fununsn1  38267  bj-fvmptunsn1  38271  topdifinffinlem  38363  relowlssretop  38379  domalom  38420  fin2solem  38622  poimirlem2  38633  poimirlem3  38634  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem8  38639  poimirlem9  38640  poimirlem13  38644  poimirlem14  38645  poimirlem15  38646  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem21  38652  poimirlem22  38653  poimirlem23  38654  poimirlem26  38657  poimirlem31  38662  mblfinlem1  38668  mblfinlem2  38669  dvasin  38715  dvacos  38716  areacirclem4  38722  ax10fromc7  40045  hdmaplem1  42921  hdmaplem2N  42922  hdmaplem3  42923  negn0nposznnd  43432  fimgmcyc  43691  irrapx1  43928  limnsuc  44360  gneispace  45227  mnuprdlem2  45350  sineq0ALT  46012  sumnnodd  46735  fperdvper  47022  stoweidlem35  47138  stirlinglem5  47181  fourierdlem68  47277  fourierswlem  47333  fouriersw  47334  iundjiunlem  47562  smfmbfcex  47863  et-ltneverrefl  47974  et-sqrtnegnre  47976  requad1  48813  requad2  48814  lmod1zrnlvec  49699  initopropdlemlem  50454  elsetrecslem  50960