Theorem nsyl 134

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 132	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 133	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  149  intnand  953  intnanrd  954  intn3an1d  1434  intn3an2d  1435  intn3an3d  1436  camestres  2558  camestros  2562  calemes  2569  calemos  2572  pssn2lp  3670  sotrieq  4986  ordnbtwn  5733  ordnbtwnOLD  5734  funun  5846  canth  6508  dfwe2  6873  pwuninel2  7287  swoer  7659  swoord1  7660  swoord2  7661  php2  8030  en3lp  8396  cantnfp1lem1  8458  cantnfp1lem3  8460  cantnflem2  8470  rankxpsuc  8628  cardmin2  8707  infxpenlem  8719  cardaleph  8795  isfin4-3  9020  fin23lem24  9027  fin23lem25  9029  fin23lem26  9030  fin23lem38  9054  isfin32i  9070  fin34  9095  fin67  9100  nd3  9290  fpwwe2lem13  9343  canthnum  9350  canthwe  9352  pwfseq  9365  gchcdaidm  9369  gchxpidm  9370  r1wunlim  9438  suplem2pr  9754  elnnz  11264  fzneuz  12290  fzodisj  12371  fzodisjsn  12374  hasheq0  13015  swrd0  13286  cnpart  13828  sqreulem  13947  rlimuni  14129  rlimcld2  14157  divalglem6  14959  bitsf1  15006  infpnlem1  15452  ramubcl  15560  ressress  15765  mreexmrid  16126  gsum2d  18194  dprddomprc  18222  ablfacrplem  18287  rng1nfld  19099  mplsubrglem  19260  mdetunilem6  20242  mdetunilem9  20245  madugsum  20268  infil  21477  fbasfip  21482  fgcl  21492  fin1aufil  21546  hauspwpwf1  21601  ovolicc2lem4  23095  ovolioo  23143  i1fima2sn  23253  itg1addlem4  23272  itgsplitioo  23410  lhop1lem  23580  chordthmlem  24359  ressatans  24461  ftalem5  24603  ppiprm  24677  chtprm  24679  lgsdir2lem2  24851  dirith2  25017  axlowdimlem13  25634  axlowdim1  25639  frgra2v  26526  eulerpartlemgvv  29765  ballotlemfp1  29880  ballotlem4  29887  ballotlemirc  29920  erdszelem8  30434  bccolsum  30878  nodenselem7  31086  nobndup  31099  nobnddown  31100  nn0prpwlem  31487  nn0prpw  31488  ivthALT  31500  nandsym1  31591  onsucsuccmpi  31612  onint1  31618  bj-xnex  32245  topdifinffinlem  32371  relowlssretop  32387  fin2solem  32565  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem26  32605  poimirlem31  32610  mblfinlem1  32616  mblfinlem2  32617  dvasin  32666  dvacos  32667  areacirclem4  32673  ax10fromc7  33198  hdmaplem1  36078  hdmaplem2N  36079  hdmaplem3  36080  irrapx1  36410  gneispace  37452  sineq0ALT  38195  sumnnodd  38697  fperdvper  38808  stoweidlem35  38928  stirlinglem5  38971  fourierdlem68  39067  fourierswlem  39123  fouriersw  39124  opabn1stprc  40318  nfrgr2v  41442  zrninitoringc  41863  lmod1zrnlvec  42077  elsetrecslem  42243