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  328  intnand  488  intnanrd  489  intn3an1d  1481  intn3an2d  1482  intn3an3d  1483  nsb  2109  necon3ai  2953  pssn2lp  4054  sotrieq  5555  ordnbtwn  6401  funun  6527  canth  7300  0mpo0  7429  dfwe2  7707  opabn1stprc  7990  pwuninel2  8204  frrlem11  8226  frrlem12  8227  swoer  8653  swoord1  8654  swoord2  8655  1sdom2dom  9138  en3lp  9504  cantnfp1lem1  9568  cantnfp1lem3  9570  cantnflem2  9580  rankxpsuc  9775  cardmin2  9892  infxpenlem  9904  cardaleph  9980  isfin4p1  10206  fin23lem24  10213  fin23lem25  10215  fin23lem26  10216  fin23lem38  10240  isfin32i  10256  fin34  10281  fin67  10286  nd3  10480  fpwwe2lem12  10533  canthnum  10540  canthwe  10542  pwfseq  10555  gchdjuidm  10559  gchxpidm  10560  r1wunlim  10628  suplem2pr  10944  elnnz  12478  fzneuz  13508  fzodisj  13593  fzodisjsn  13597  hasheq0  14270  swrd0  14566  cnpart  15147  sqreulem  15267  rlimuni  15457  rlimcld2  15485  divalglem6  16309  bitsf1  16357  infpnlem1  16822  ramubcl  16930  ressress  17158  mreexmrid  17549  gsum2d  19885  dprddomprc  19915  ablfacrplem  19980  trivnsimpgd  20012  ablsimpnosubgd  20019  zrninitoringc  20592  rng1nfld  20695  mplsubrglem  21942  mdetunilem6  22533  mdetunilem9  22536  madugsum  22559  infil  23779  fbasfip  23784  fgcl  23794  fin1aufil  23848  hauspwpwf1  23903  ovolicc2lem4  25449  ovolioo  25497  i1fima2sn  25609  itg1addlem4  25628  itgsplitioo  25767  lhop1lem  25946  chordthmlem  26770  ressatans  26872  ftalem5  27015  ppiprm  27089  chtprm  27091  lgsdir2lem2  27265  dirith2  27467  noresle  27637  noetasuplem4  27676  noetainflem4  27680  elnnzs  28326  axlowdimlem13  28933  axlowdim1  28938  nfrgr2v  30250  gsumfs2d  33033  ply1annnr  33714  inelpisys  34165  eulerpartlemgvv  34387  ballotlemfp1  34503  ballotlem4  34510  ballotlemirc  34543  erdszelem8  35240  bccolsum  35781  nn0prpwlem  36362  nn0prpw  36363  ivthALT  36375  nandsym1  36462  onsucsuccmpi  36483  onint1  36489  weiunpo  36505  bj-fununsn1  37293  bj-fvmptunsn1  37297  topdifinffinlem  37387  relowlssretop  37403  domalom  37444  fin2solem  37652  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem9  37675  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem26  37692  poimirlem31  37697  mblfinlem1  37703  mblfinlem2  37704  dvasin  37750  dvacos  37751  areacirclem4  37757  ax10fromc7  38940  hdmaplem1  41816  hdmaplem2N  41817  hdmaplem3  41818  negn0nposznnd  42321  fimgmcyc  42573  irrapx1  42867  limnsuc  43304  gneispace  44173  mnuprdlem2  44312  sineq0ALT  44975  sumnnodd  45676  fperdvper  45963  stoweidlem35  46079  stirlinglem5  46122  fourierdlem68  46218  fourierswlem  46274  fouriersw  46275  iundjiunlem  46503  smfmbfcex  46804  et-ltneverrefl  46915  et-sqrtnegnre  46917  requad1  47659  requad2  47660  lmod1zrnlvec  48532  initopropdlemlem  49277  elsetrecslem  49737