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 ⊢ (𝜑 → ¬ 𝜒)

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  155  sylnib  331  intnand  493  intnanrd  494  intn3an1d  1503  intn3an2d  1504  intn3an3d  1505  nsb  2143  necon3ai  2985  pssn2lp  4061  sotrieq  5590  ordnbtwn  6445  funun  6571  canth  7354  0mpo0  7483  dfwe2  7761  opabn1stprc  8043  pwuninel2  8258  frrlem11  8281  frrlem12  8282  swoer  8714  swoord1  8715  swoord2  8716  1sdom2dom  9202  en3lp  9571  cantnfp1lem1  9635  cantnfp1lem3  9637  cantnflem2  9647  rankxpsuc  9842  cardmin2  9973  infxpenlem  9985  cardaleph  10061  isfin4p1  10287  fin23lem24  10294  fin23lem25  10296  fin23lem26  10297  fin23lem38  10321  isfin32i  10337  fin34  10362  fin67  10367  nd3  10562  fpwwe2lem12  10615  canthnum  10622  canthwe  10624  pwfseq  10637  gchdjuidm  10641  gchxpidm  10642  r1wunlim  10710  suplem2pr  11026  elnnz  12589  fzneuz  13624  fzodisj  13710  fzodisjsn  13714  hasheq0  14387  swrd0  14684  cnpart  15279  sqreulem  15399  rlimuni  15589  rlimcld2  15617  divalglem6  16444  bitsf1  16492  infpnlem1  16958  ramubcl  17066  ressress  17295  mreexmrid  17687  gsum2d  20030  dprddomprc  20060  ablfacrplem  20125  trivnsimpgd  20157  ablsimpnosubgd  20164  zrninitoringc  20749  rng1nfld  20848  mplsubrglem  22110  mdetunilem6  22731  mdetunilem9  22734  madugsum  22757  infil  23977  fbasfip  23982  fgcl  23992  fin1aufil  24046  hauspwpwf1  24101  ovolicc2lem4  25636  ovolioo  25684  i1fima2sn  25796  itg1addlem4  25815  itgsplitioo  25954  lhop1lem  26129  chordthmlem  26951  ressatans  27053  ftalem5  27195  ppiprm  27269  chtprm  27271  lgsdir2lem2  27444  dirith2  27646  noresle  27815  noetasuplem4  27854  noetainflem4  27858  elnnzs  28548  axlowdimlem13  29209  axlowdim1  29214  nfrgr2v  30528  gsumfs2d  33289  ply1annnr  34005  inelpisys  34456  eulerpartlemgvv  34678  ballotlemfp1  34794  ballotlem4  34801  ballotlemirc  34834  erdszelem8  35556  bccolsum  36097  nn0prpwlem  36690  nn0prpw  36691  ivthALT  36703  nandsym1  36790  onsucsuccmpi  36811  onint1  36817  weiunpo  36833  bj-fununsn1  37752  bj-fvmptunsn1  37756  topdifinffinlem  37848  relowlssretop  37864  domalom  37905  fin2solem  38112  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem9  38135  poimirlem13  38139  poimirlem14  38140  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem21  38147  poimirlem22  38148  poimirlem23  38149  poimirlem26  38152  poimirlem31  38157  mblfinlem1  38163  mblfinlem2  38164  dvasin  38210  dvacos  38211  areacirclem4  38217  ax10fromc7  39526  hdmaplem1  42402  hdmaplem2N  42403  hdmaplem3  42404  negn0nposznnd  42898  fimgmcyc  43159  irrapx1  43412  limnsuc  43849  gneispace  44717  mnuprdlem2  44842  sineq0ALT  45504  sumnnodd  46205  fperdvper  46492  stoweidlem35  46608  stirlinglem5  46651  fourierdlem68  46747  fourierswlem  46803  fouriersw  46804  iundjiunlem  47032  smfmbfcex  47333  et-ltneverrefl  47444  et-sqrtnegnre  47446  requad1  48243  requad2  48244  lmod1zrnlvec  49126  initopropdlemlem  49869  elsetrecslem  50329