Theorem nsyl 140

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 138	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 139	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  con3i  154  sylnib  327  intnand  487  intnanrd  488  intn3an1d  1476  intn3an2d  1477  intn3an3d  1478  nsb  2098  necon3ai  2958  pssn2lp  4108  sotrieq  5625  ordnbtwn  6471  funun  6607  canth  7380  0mpo0  7511  dfwe2  7787  opabn1stprc  8077  pwuninel2  8293  frrlem11  8315  frrlem12  8316  swoer  8769  swoord1  8770  swoord2  8771  php2OLD  9261  phpeqdOLD  9263  1sdom2dom  9285  en3lp  9658  cantnfp1lem1  9722  cantnfp1lem3  9724  cantnflem2  9734  rankxpsuc  9926  cardmin2  10043  infxpenlem  10057  cardaleph  10133  isfin4p1  10359  fin23lem24  10366  fin23lem25  10368  fin23lem26  10369  fin23lem38  10393  isfin32i  10409  fin34  10434  fin67  10439  nd3  10633  fpwwe2lem12  10686  canthnum  10693  canthwe  10695  pwfseq  10708  gchdjuidm  10712  gchxpidm  10713  r1wunlim  10781  suplem2pr  11097  elnnz  12624  fzneuz  13640  fzodisj  13724  fzodisjsn  13728  hasheq0  14386  swrd0  14679  cnpart  15258  sqreulem  15377  rlimuni  15565  rlimcld2  15593  divalglem6  16413  bitsf1  16459  infpnlem1  16925  ramubcl  17033  ressress  17275  mreexmrid  17669  gsum2d  19982  dprddomprc  20012  ablfacrplem  20077  trivnsimpgd  20109  ablsimpnosubgd  20116  zrninitoringc  20666  rng1nfld  20770  mplsubrglem  22014  mdetunilem6  22610  mdetunilem9  22613  madugsum  22636  infil  23858  fbasfip  23863  fgcl  23873  fin1aufil  23927  hauspwpwf1  23982  ovolicc2lem4  25540  ovolioo  25588  i1fima2sn  25700  itg1addlem4  25719  itg1addlem4OLD  25720  itgsplitioo  25858  lhop1lem  26037  chordthmlem  26857  ressatans  26959  ftalem5  27102  ppiprm  27176  chtprm  27178  lgsdir2lem2  27352  dirith2  27554  noresle  27724  noetasuplem4  27763  noetainflem4  27767  elnnzs  28354  axlowdimlem13  28930  axlowdim1  28935  nfrgr2v  30247  ply1annnr  33641  inelpisys  34063  eulerpartlemgvv  34286  ballotlemfp1  34401  ballotlem4  34408  ballotlemirc  34441  erdszelem8  35111  bccolsum  35646  nn0prpwlem  36120  nn0prpw  36121  ivthALT  36133  nandsym1  36220  onsucsuccmpi  36241  onint1  36247  bj-fununsn1  37045  bj-fvmptunsn1  37049  topdifinffinlem  37139  relowlssretop  37155  domalom  37196  fin2solem  37392  poimirlem2  37408  poimirlem3  37409  poimirlem4  37410  poimirlem6  37412  poimirlem7  37413  poimirlem8  37414  poimirlem9  37415  poimirlem13  37419  poimirlem14  37420  poimirlem15  37421  poimirlem16  37422  poimirlem17  37423  poimirlem19  37425  poimirlem20  37426  poimirlem21  37427  poimirlem22  37428  poimirlem23  37429  poimirlem26  37432  poimirlem31  37437  mblfinlem1  37443  mblfinlem2  37444  dvasin  37490  dvacos  37491  areacirclem4  37497  ax10fromc7  38678  hdmaplem1  41555  hdmaplem2N  41556  hdmaplem3  41557  negn0nposznnd  42096  fimgmcyc  42299  irrapx1  42597  limnsuc  43043  gneispace  43913  mnuprdlem2  44059  sineq0ALT  44725  sumnnodd  45362  fperdvper  45651  stoweidlem35  45767  stirlinglem5  45810  fourierdlem68  45906  fourierswlem  45962  fouriersw  45963  iundjiunlem  46191  smfmbfcex  46492  et-ltneverrefl  46603  et-sqrtnegnre  46605  singoutnupword  46613  tworepnotupword  46616  requad1  47305  requad2  47306  lmod1zrnlvec  47999  elsetrecslem  48567