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  488  intnanrd  489  intn3an1d  1477  intn3an2d  1478  intn3an3d  1479  nsb  2106  necon3ai  2967  pssn2lp  4032  sotrieq  5523  ordnbtwn  6341  funun  6464  canth  7209  0mpo0  7336  dfwe2  7602  opabn1stprc  7871  pwuninel2  8061  frrlem11  8083  frrlem12  8084  swoer  8486  swoord1  8487  swoord2  8488  php2  8898  phpeqd  8902  en3lp  9302  cantnfp1lem1  9366  cantnfp1lem3  9368  cantnflem2  9378  rankxpsuc  9571  cardmin2  9688  infxpenlem  9700  cardaleph  9776  isfin4p1  10002  fin23lem24  10009  fin23lem25  10011  fin23lem26  10012  fin23lem38  10036  isfin32i  10052  fin34  10077  fin67  10082  nd3  10276  fpwwe2lem12  10329  canthnum  10336  canthwe  10338  pwfseq  10351  gchdjuidm  10355  gchxpidm  10356  r1wunlim  10424  suplem2pr  10740  elnnz  12259  fzneuz  13266  fzodisj  13349  fzodisjsn  13353  hasheq0  14006  swrd0  14299  cnpart  14879  sqreulem  14999  rlimuni  15187  rlimcld2  15215  divalglem6  16035  bitsf1  16081  infpnlem1  16539  ramubcl  16647  ressress  16884  mreexmrid  17269  gsum2d  19488  dprddomprc  19518  ablfacrplem  19583  trivnsimpgd  19615  ablsimpnosubgd  19622  rng1nfld  20462  mplsubrglem  21120  mdetunilem6  21674  mdetunilem9  21677  madugsum  21700  infil  22922  fbasfip  22927  fgcl  22937  fin1aufil  22991  hauspwpwf1  23046  ovolicc2lem4  24589  ovolioo  24637  i1fima2sn  24749  itg1addlem4  24768  itg1addlem4OLD  24769  itgsplitioo  24907  lhop1lem  25082  chordthmlem  25887  ressatans  25989  ftalem5  26131  ppiprm  26205  chtprm  26207  lgsdir2lem2  26379  dirith2  26581  axlowdimlem13  27225  axlowdim1  27230  nfrgr2v  28537  inelpisys  32022  eulerpartlemgvv  32243  ballotlemfp1  32358  ballotlem4  32365  ballotlemirc  32398  erdszelem8  33060  bccolsum  33611  noresle  33827  noetasuplem4  33866  noetainflem4  33870  nn0prpwlem  34438  nn0prpw  34439  ivthALT  34451  nandsym1  34538  onsucsuccmpi  34559  onint1  34565  bj-fununsn1  35351  bj-fvmptunsn1  35355  topdifinffinlem  35445  relowlssretop  35461  domalom  35502  fin2solem  35690  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem26  35730  poimirlem31  35735  mblfinlem1  35741  mblfinlem2  35742  dvasin  35788  dvacos  35789  areacirclem4  35795  ax10fromc7  36836  hdmaplem1  39712  hdmaplem2N  39713  hdmaplem3  39714  negn0nposznnd  40231  irrapx1  40566  gneispace  41633  mnuprdlem2  41780  sineq0ALT  42446  sumnnodd  43061  fperdvper  43350  stoweidlem35  43466  stirlinglem5  43509  fourierdlem68  43605  fourierswlem  43661  fouriersw  43662  iundjiunlem  43887  smfmbfcex  44182  requad1  44962  requad2  44963  zrninitoringc  45517  lmod1zrnlvec  45723  elsetrecslem  46290