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  4077  sotrieq  5496  ordnbtwn  6275  funun  6394  canth  7105  0mpo0  7231  dfwe2  7490  opabn1stprc  7750  pwuninel2  7934  swoer  8313  swoord1  8314  swoord2  8315  php2  8696  phpeqd  8700  en3lp  9071  cantnfp1lem1  9135  cantnfp1lem3  9137  cantnflem2  9147  rankxpsuc  9305  cardmin2  9421  infxpenlem  9433  cardaleph  9509  isfin4p1  9731  fin23lem24  9738  fin23lem25  9740  fin23lem26  9741  fin23lem38  9765  isfin32i  9781  fin34  9806  fin67  9811  nd3  10005  fpwwe2lem13  10058  canthnum  10065  canthwe  10067  pwfseq  10080  gchdjuidm  10084  gchxpidm  10085  r1wunlim  10153  suplem2pr  10469  elnnz  11985  fzneuz  12982  fzodisj  13065  fzodisjsn  13069  hasheq0  13718  swrd0  14014  cnpart  14593  sqreulem  14713  rlimuni  14901  rlimcld2  14929  divalglem6  15743  bitsf1  15789  infpnlem1  16240  ramubcl  16348  ressress  16556  mreexmrid  16908  gsum2d  19086  dprddomprc  19116  ablfacrplem  19181  trivnsimpgd  19213  ablsimpnosubgd  19220  rng1nfld  20045  mplsubrglem  20213  mdetunilem6  21220  mdetunilem9  21223  madugsum  21246  infil  22465  fbasfip  22470  fgcl  22480  fin1aufil  22534  hauspwpwf1  22589  ovolicc2lem4  24115  ovolioo  24163  i1fima2sn  24275  itg1addlem4  24294  itgsplitioo  24432  lhop1lem  24604  chordthmlem  25404  ressatans  25506  ftalem5  25648  ppiprm  25722  chtprm  25724  lgsdir2lem2  25896  dirith2  26098  axlowdimlem13  26734  axlowdim1  26739  nfrgr2v  28045  eulerpartlemgvv  31629  ballotlemfp1  31744  ballotlem4  31751  ballotlemirc  31784  erdszelem8  32440  bccolsum  32966  frrlem11  33128  frrlem12  33129  noresle  33195  noetalem3  33214  nn0prpwlem  33665  nn0prpw  33666  ivthALT  33678  nandsym1  33765  onsucsuccmpi  33786  onint1  33792  bj-fununsn1  34529  bj-fvmptunsn1  34533  topdifinffinlem  34622  relowlssretop  34638  domalom  34679  fin2solem  34872  poimirlem2  34888  poimirlem3  34889  poimirlem4  34890  poimirlem6  34892  poimirlem7  34893  poimirlem8  34894  poimirlem9  34895  poimirlem13  34899  poimirlem14  34900  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem23  34909  poimirlem26  34912  poimirlem31  34917  mblfinlem1  34923  mblfinlem2  34924  dvasin  34972  dvacos  34973  areacirclem4  34979  ax10fromc7  36025  hdmaplem1  38901  hdmaplem2N  38902  hdmaplem3  38903  negn0nposznnd  39161  irrapx1  39418  gneispace  40477  mnuprdlem2  40602  sineq0ALT  41264  sumnnodd  41904  fperdvper  42196  stoweidlem35  42314  stirlinglem5  42357  fourierdlem68  42453  fourierswlem  42509  fouriersw  42510  requad1  43781  requad2  43782  zrninitoringc  44336  lmod1zrnlvec  44543  elsetrecslem  44795