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  490  intnanrd  491  intn3an1d  1480  intn3an2d  1481  intn3an3d  1482  nsb  2105  necon3ai  2966  pssn2lp  4102  sotrieq  5618  ordnbtwn  6458  funun  6595  canth  7362  0mpo0  7492  dfwe2  7761  opabn1stprc  8044  pwuninel2  8259  frrlem11  8281  frrlem12  8282  swoer  8733  swoord1  8734  swoord2  8735  php2OLD  9223  phpeqdOLD  9225  1sdom2dom  9247  en3lp  9609  cantnfp1lem1  9673  cantnfp1lem3  9675  cantnflem2  9685  rankxpsuc  9877  cardmin2  9994  infxpenlem  10008  cardaleph  10084  isfin4p1  10310  fin23lem24  10317  fin23lem25  10319  fin23lem26  10320  fin23lem38  10344  isfin32i  10360  fin34  10385  fin67  10390  nd3  10584  fpwwe2lem12  10637  canthnum  10644  canthwe  10646  pwfseq  10659  gchdjuidm  10663  gchxpidm  10664  r1wunlim  10732  suplem2pr  11048  elnnz  12568  fzneuz  13582  fzodisj  13666  fzodisjsn  13670  hasheq0  14323  swrd0  14608  cnpart  15187  sqreulem  15306  rlimuni  15494  rlimcld2  15522  divalglem6  16341  bitsf1  16387  infpnlem1  16843  ramubcl  16951  ressress  17193  mreexmrid  17587  gsum2d  19840  dprddomprc  19870  ablfacrplem  19935  trivnsimpgd  19967  ablsimpnosubgd  19974  rng1nfld  20400  mplsubrglem  21563  mdetunilem6  22119  mdetunilem9  22122  madugsum  22145  infil  23367  fbasfip  23372  fgcl  23382  fin1aufil  23436  hauspwpwf1  23491  ovolicc2lem4  25037  ovolioo  25085  i1fima2sn  25197  itg1addlem4  25216  itg1addlem4OLD  25217  itgsplitioo  25355  lhop1lem  25530  chordthmlem  26337  ressatans  26439  ftalem5  26581  ppiprm  26655  chtprm  26657  lgsdir2lem2  26829  dirith2  27031  noresle  27200  noetasuplem4  27239  noetainflem4  27243  axlowdimlem13  28212  axlowdim1  28217  nfrgr2v  29525  ply1annnr  32764  inelpisys  33152  eulerpartlemgvv  33375  ballotlemfp1  33490  ballotlem4  33497  ballotlemirc  33530  erdszelem8  34189  bccolsum  34709  nn0prpwlem  35207  nn0prpw  35208  ivthALT  35220  nandsym1  35307  onsucsuccmpi  35328  onint1  35334  bj-fununsn1  36134  bj-fvmptunsn1  36138  topdifinffinlem  36228  relowlssretop  36244  domalom  36285  fin2solem  36474  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem26  36514  poimirlem31  36519  mblfinlem1  36525  mblfinlem2  36526  dvasin  36572  dvacos  36573  areacirclem4  36579  ax10fromc7  37765  hdmaplem1  40642  hdmaplem2N  40643  hdmaplem3  40644  negn0nposznnd  41194  irrapx1  41566  limnsuc  42015  gneispace  42885  mnuprdlem2  43032  sineq0ALT  43698  sumnnodd  44346  fperdvper  44635  stoweidlem35  44751  stirlinglem5  44794  fourierdlem68  44890  fourierswlem  44946  fouriersw  44947  iundjiunlem  45175  smfmbfcex  45476  et-ltneverrefl  45587  et-sqrtnegnre  45589  singoutnupword  45597  tworepnotupword  45600  requad1  46290  requad2  46291  zrninitoringc  46969  lmod1zrnlvec  47175  elsetrecslem  47744