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  489  intnanrd  490  intn3an1d  1479  intn3an2d  1480  intn3an3d  1481  nsb  2104  necon3ai  2965  pssn2lp  4101  sotrieq  5617  ordnbtwn  6457  funun  6594  canth  7361  0mpo0  7491  dfwe2  7760  opabn1stprc  8043  pwuninel2  8258  frrlem11  8280  frrlem12  8281  swoer  8732  swoord1  8733  swoord2  8734  php2OLD  9222  phpeqdOLD  9224  1sdom2dom  9246  en3lp  9608  cantnfp1lem1  9672  cantnfp1lem3  9674  cantnflem2  9684  rankxpsuc  9876  cardmin2  9993  infxpenlem  10007  cardaleph  10083  isfin4p1  10309  fin23lem24  10316  fin23lem25  10318  fin23lem26  10319  fin23lem38  10343  isfin32i  10359  fin34  10384  fin67  10389  nd3  10583  fpwwe2lem12  10636  canthnum  10643  canthwe  10645  pwfseq  10658  gchdjuidm  10662  gchxpidm  10663  r1wunlim  10731  suplem2pr  11047  elnnz  12567  fzneuz  13581  fzodisj  13665  fzodisjsn  13669  hasheq0  14322  swrd0  14607  cnpart  15186  sqreulem  15305  rlimuni  15493  rlimcld2  15521  divalglem6  16340  bitsf1  16386  infpnlem1  16842  ramubcl  16950  ressress  17192  mreexmrid  17586  gsum2d  19839  dprddomprc  19869  ablfacrplem  19934  trivnsimpgd  19966  ablsimpnosubgd  19973  rng1nfld  20399  mplsubrglem  21562  mdetunilem6  22118  mdetunilem9  22121  madugsum  22144  infil  23366  fbasfip  23371  fgcl  23381  fin1aufil  23435  hauspwpwf1  23490  ovolicc2lem4  25036  ovolioo  25084  i1fima2sn  25196  itg1addlem4  25215  itg1addlem4OLD  25216  itgsplitioo  25354  lhop1lem  25529  chordthmlem  26334  ressatans  26436  ftalem5  26578  ppiprm  26652  chtprm  26654  lgsdir2lem2  26826  dirith2  27028  noresle  27197  noetasuplem4  27236  noetainflem4  27240  axlowdimlem13  28209  axlowdim1  28214  nfrgr2v  29522  ply1annnr  32759  inelpisys  33147  eulerpartlemgvv  33370  ballotlemfp1  33485  ballotlem4  33492  ballotlemirc  33525  erdszelem8  34184  bccolsum  34704  nn0prpwlem  35202  nn0prpw  35203  ivthALT  35215  nandsym1  35302  onsucsuccmpi  35323  onint1  35329  bj-fununsn1  36129  bj-fvmptunsn1  36133  topdifinffinlem  36223  relowlssretop  36239  domalom  36280  fin2solem  36469  poimirlem2  36485  poimirlem3  36486  poimirlem4  36487  poimirlem6  36489  poimirlem7  36490  poimirlem8  36491  poimirlem9  36492  poimirlem13  36496  poimirlem14  36497  poimirlem15  36498  poimirlem16  36499  poimirlem17  36500  poimirlem19  36502  poimirlem20  36503  poimirlem21  36504  poimirlem22  36505  poimirlem23  36506  poimirlem26  36509  poimirlem31  36514  mblfinlem1  36520  mblfinlem2  36521  dvasin  36567  dvacos  36568  areacirclem4  36574  ax10fromc7  37760  hdmaplem1  40637  hdmaplem2N  40638  hdmaplem3  40639  negn0nposznnd  41196  irrapx1  41556  limnsuc  42005  gneispace  42875  mnuprdlem2  43022  sineq0ALT  43688  sumnnodd  44336  fperdvper  44625  stoweidlem35  44741  stirlinglem5  44784  fourierdlem68  44880  fourierswlem  44936  fouriersw  44937  iundjiunlem  45165  smfmbfcex  45466  et-ltneverrefl  45577  et-sqrtnegnre  45579  singoutnupword  45587  tworepnotupword  45590  requad1  46280  requad2  46281  zrninitoringc  46959  lmod1zrnlvec  47165  elsetrecslem  47734