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  330  intnand  491  intnanrd  492  intn3an1d  1475  intn3an2d  1476  intn3an3d  1477  pssn2lp  4080  sotrieq  5504  ordnbtwn  6283  funun  6402  canth  7113  0mpo0  7239  dfwe2  7498  opabn1stprc  7758  pwuninel2  7942  swoer  8321  swoord1  8322  swoord2  8323  php2  8704  phpeqd  8708  en3lp  9079  cantnfp1lem1  9143  cantnfp1lem3  9145  cantnflem2  9155  rankxpsuc  9313  cardmin2  9429  infxpenlem  9441  cardaleph  9517  isfin4p1  9739  fin23lem24  9746  fin23lem25  9748  fin23lem26  9749  fin23lem38  9773  isfin32i  9789  fin34  9814  fin67  9819  nd3  10013  fpwwe2lem13  10066  canthnum  10073  canthwe  10075  pwfseq  10088  gchdjuidm  10092  gchxpidm  10093  r1wunlim  10161  suplem2pr  10477  elnnz  11994  fzneuz  12991  fzodisj  13074  fzodisjsn  13078  hasheq0  13727  swrd0  14022  cnpart  14601  sqreulem  14721  rlimuni  14909  rlimcld2  14937  divalglem6  15751  bitsf1  15797  infpnlem1  16248  ramubcl  16356  ressress  16564  mreexmrid  16916  gsum2d  19094  dprddomprc  19124  ablfacrplem  19189  trivnsimpgd  19221  ablsimpnosubgd  19228  rng1nfld  20053  mplsubrglem  20221  mdetunilem6  21228  mdetunilem9  21231  madugsum  21254  infil  22473  fbasfip  22478  fgcl  22488  fin1aufil  22542  hauspwpwf1  22597  ovolicc2lem4  24123  ovolioo  24171  i1fima2sn  24283  itg1addlem4  24302  itgsplitioo  24440  lhop1lem  24612  chordthmlem  25412  ressatans  25514  ftalem5  25656  ppiprm  25730  chtprm  25732  lgsdir2lem2  25904  dirith2  26106  axlowdimlem13  26742  axlowdim1  26747  nfrgr2v  28053  eulerpartlemgvv  31636  ballotlemfp1  31751  ballotlem4  31758  ballotlemirc  31791  erdszelem8  32447  bccolsum  32973  frrlem11  33135  frrlem12  33136  noresle  33202  noetalem3  33221  nn0prpwlem  33672  nn0prpw  33673  ivthALT  33685  nandsym1  33772  onsucsuccmpi  33793  onint1  33799  bj-fununsn1  34537  bj-fvmptunsn1  34541  topdifinffinlem  34630  relowlssretop  34646  domalom  34687  fin2solem  34880  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem23  34917  poimirlem26  34920  poimirlem31  34925  mblfinlem1  34931  mblfinlem2  34932  dvasin  34980  dvacos  34981  areacirclem4  34987  ax10fromc7  36033  hdmaplem1  38909  hdmaplem2N  38910  hdmaplem3  38911  negn0nposznnd  39175  irrapx1  39432  gneispace  40491  mnuprdlem2  40616  sineq0ALT  41278  sumnnodd  41918  fperdvper  42210  stoweidlem35  42327  stirlinglem5  42370  fourierdlem68  42466  fourierswlem  42522  fouriersw  42523  requad1  43794  requad2  43795  zrninitoringc  44349  lmod1zrnlvec  44556  elsetrecslem  44808