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  489  intnanrd  490  intn3an1d  1478  intn3an2d  1479  intn3an3d  1480  nsb  2105  necon3ai  2969  pssn2lp  4037  sotrieq  5533  ordnbtwn  6360  funun  6487  canth  7238  0mpo0  7367  dfwe2  7633  opabn1stprc  7907  pwuninel2  8099  frrlem11  8121  frrlem12  8122  swoer  8537  swoord1  8538  swoord2  8539  php2OLD  9015  phpeqdOLD  9017  en3lp  9381  cantnfp1lem1  9445  cantnfp1lem3  9447  cantnflem2  9457  rankxpsuc  9649  cardmin2  9766  infxpenlem  9778  cardaleph  9854  isfin4p1  10080  fin23lem24  10087  fin23lem25  10089  fin23lem26  10090  fin23lem38  10114  isfin32i  10130  fin34  10155  fin67  10160  nd3  10354  fpwwe2lem12  10407  canthnum  10414  canthwe  10416  pwfseq  10429  gchdjuidm  10433  gchxpidm  10434  r1wunlim  10502  suplem2pr  10818  elnnz  12338  fzneuz  13346  fzodisj  13430  fzodisjsn  13434  hasheq0  14087  swrd0  14380  cnpart  14960  sqreulem  15080  rlimuni  15268  rlimcld2  15296  divalglem6  16116  bitsf1  16162  infpnlem1  16620  ramubcl  16728  ressress  16967  mreexmrid  17361  gsum2d  19582  dprddomprc  19612  ablfacrplem  19677  trivnsimpgd  19709  ablsimpnosubgd  19716  rng1nfld  20558  mplsubrglem  21219  mdetunilem6  21775  mdetunilem9  21778  madugsum  21801  infil  23023  fbasfip  23028  fgcl  23038  fin1aufil  23092  hauspwpwf1  23147  ovolicc2lem4  24693  ovolioo  24741  i1fima2sn  24853  itg1addlem4  24872  itg1addlem4OLD  24873  itgsplitioo  25011  lhop1lem  25186  chordthmlem  25991  ressatans  26093  ftalem5  26235  ppiprm  26309  chtprm  26311  lgsdir2lem2  26483  dirith2  26685  axlowdimlem13  27331  axlowdim1  27336  nfrgr2v  28645  inelpisys  32131  eulerpartlemgvv  32352  ballotlemfp1  32467  ballotlem4  32474  ballotlemirc  32507  erdszelem8  33169  bccolsum  33714  noresle  33909  noetasuplem4  33948  noetainflem4  33952  nn0prpwlem  34520  nn0prpw  34521  ivthALT  34533  nandsym1  34620  onsucsuccmpi  34641  onint1  34647  bj-fununsn1  35433  bj-fvmptunsn1  35437  topdifinffinlem  35527  relowlssretop  35543  domalom  35584  fin2solem  35772  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem9  35795  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem26  35812  poimirlem31  35817  mblfinlem1  35823  mblfinlem2  35824  dvasin  35870  dvacos  35871  areacirclem4  35877  ax10fromc7  36916  hdmaplem1  39792  hdmaplem2N  39793  hdmaplem3  39794  negn0nposznnd  40317  irrapx1  40657  gneispace  41751  mnuprdlem2  41898  sineq0ALT  42564  sumnnodd  43178  fperdvper  43467  stoweidlem35  43583  stirlinglem5  43626  fourierdlem68  43722  fourierswlem  43778  fouriersw  43779  iundjiunlem  44004  smfmbfcex  44305  requad1  45085  requad2  45086  zrninitoringc  45640  lmod1zrnlvec  45846  elsetrecslem  46415  et-ltneverrefl  46521  singoutnupword  46529  tworepnotupword  46532