Theorem nsyl 142

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 140	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 141	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  157  sylnib  331  intnand  492  intnanrd  493  intn3an1d  1481  intn3an2d  1482  intn3an3d  1483  nsb  2108  necon3ai  2965  pssn2lp  4016  sotrieq  5497  ordnbtwn  6303  funun  6426  canth  7167  0mpo0  7294  dfwe2  7559  opabn1stprc  7828  pwuninel2  8016  frrlem11  8037  frrlem12  8038  swoer  8421  swoord1  8422  swoord2  8423  php2  8831  phpeqd  8835  en3lp  9229  cantnfp1lem1  9293  cantnfp1lem3  9295  cantnflem2  9305  rankxpsuc  9498  cardmin2  9615  infxpenlem  9627  cardaleph  9703  isfin4p1  9929  fin23lem24  9936  fin23lem25  9938  fin23lem26  9939  fin23lem38  9963  isfin32i  9979  fin34  10004  fin67  10009  nd3  10203  fpwwe2lem12  10256  canthnum  10263  canthwe  10265  pwfseq  10278  gchdjuidm  10282  gchxpidm  10283  r1wunlim  10351  suplem2pr  10667  elnnz  12186  fzneuz  13193  fzodisj  13276  fzodisjsn  13280  hasheq0  13930  swrd0  14223  cnpart  14803  sqreulem  14923  rlimuni  15111  rlimcld2  15139  divalglem6  15959  bitsf1  16005  infpnlem1  16463  ramubcl  16571  ressress  16799  mreexmrid  17146  gsum2d  19357  dprddomprc  19387  ablfacrplem  19452  trivnsimpgd  19484  ablsimpnosubgd  19491  rng1nfld  20316  mplsubrglem  20966  mdetunilem6  21514  mdetunilem9  21517  madugsum  21540  infil  22760  fbasfip  22765  fgcl  22775  fin1aufil  22829  hauspwpwf1  22884  ovolicc2lem4  24417  ovolioo  24465  i1fima2sn  24577  itg1addlem4  24596  itg1addlem4OLD  24597  itgsplitioo  24735  lhop1lem  24910  chordthmlem  25715  ressatans  25817  ftalem5  25959  ppiprm  26033  chtprm  26035  lgsdir2lem2  26207  dirith2  26409  axlowdimlem13  27045  axlowdim1  27050  nfrgr2v  28355  inelpisys  31834  eulerpartlemgvv  32055  ballotlemfp1  32170  ballotlem4  32177  ballotlemirc  32210  erdszelem8  32873  bccolsum  33423  noresle  33637  noetasuplem4  33676  noetainflem4  33680  nn0prpwlem  34248  nn0prpw  34249  ivthALT  34261  nandsym1  34348  onsucsuccmpi  34369  onint1  34375  bj-fununsn1  35159  bj-fvmptunsn1  35163  topdifinffinlem  35255  relowlssretop  35271  domalom  35312  fin2solem  35500  poimirlem2  35516  poimirlem3  35517  poimirlem4  35518  poimirlem6  35520  poimirlem7  35521  poimirlem8  35522  poimirlem9  35523  poimirlem13  35527  poimirlem14  35528  poimirlem15  35529  poimirlem16  35530  poimirlem17  35531  poimirlem19  35533  poimirlem20  35534  poimirlem21  35535  poimirlem22  35536  poimirlem23  35537  poimirlem26  35540  poimirlem31  35545  mblfinlem1  35551  mblfinlem2  35552  dvasin  35598  dvacos  35599  areacirclem4  35605  ax10fromc7  36646  hdmaplem1  39522  hdmaplem2N  39523  hdmaplem3  39524  negn0nposznnd  40017  irrapx1  40353  gneispace  41421  mnuprdlem2  41564  sineq0ALT  42230  sumnnodd  42846  fperdvper  43135  stoweidlem35  43251  stirlinglem5  43294  fourierdlem68  43390  fourierswlem  43446  fouriersw  43447  iundjiunlem  43672  smfmbfcex  43967  requad1  44747  requad2  44748  zrninitoringc  45302  lmod1zrnlvec  45508  elsetrecslem  46075