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  4051  sotrieq  5553  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  19884  dprddomprc  19914  ablfacrplem  19979  trivnsimpgd  20011  ablsimpnosubgd  20018  zrninitoringc  20591  rng1nfld  20694  mplsubrglem  21941  mdetunilem6  22532  mdetunilem9  22535  madugsum  22558  infil  23778  fbasfip  23783  fgcl  23793  fin1aufil  23847  hauspwpwf1  23902  ovolicc2lem4  25448  ovolioo  25496  i1fima2sn  25608  itg1addlem4  25627  itgsplitioo  25766  lhop1lem  25945  chordthmlem  26769  ressatans  26871  ftalem5  27014  ppiprm  27088  chtprm  27090  lgsdir2lem2  27264  dirith2  27466  noresle  27636  noetasuplem4  27675  noetainflem4  27679  elnnzs  28325  axlowdimlem13  28932  axlowdim1  28937  nfrgr2v  30252  gsumfs2d  33035  ply1annnr  33716  inelpisys  34167  eulerpartlemgvv  34389  ballotlemfp1  34505  ballotlem4  34512  ballotlemirc  34545  erdszelem8  35242  bccolsum  35783  nn0prpwlem  36366  nn0prpw  36367  ivthALT  36379  nandsym1  36466  onsucsuccmpi  36487  onint1  36493  weiunpo  36509  bj-fununsn1  37297  bj-fvmptunsn1  37301  topdifinffinlem  37391  relowlssretop  37407  domalom  37448  fin2solem  37645  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem6  37665  poimirlem7  37666  poimirlem8  37667  poimirlem9  37668  poimirlem13  37672  poimirlem14  37673  poimirlem15  37674  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem21  37680  poimirlem22  37681  poimirlem23  37682  poimirlem26  37685  poimirlem31  37690  mblfinlem1  37696  mblfinlem2  37697  dvasin  37743  dvacos  37744  areacirclem4  37750  ax10fromc7  38993  hdmaplem1  41869  hdmaplem2N  41870  hdmaplem3  41871  negn0nposznnd  42374  fimgmcyc  42626  irrapx1  42920  limnsuc  43357  gneispace  44226  mnuprdlem2  44365  sineq0ALT  45028  sumnnodd  45729  fperdvper  46016  stoweidlem35  46132  stirlinglem5  46175  fourierdlem68  46271  fourierswlem  46327  fouriersw  46328  iundjiunlem  46556  smfmbfcex  46857  et-ltneverrefl  46968  et-sqrtnegnre  46970  requad1  47721  requad2  47722  lmod1zrnlvec  48594  initopropdlemlem  49339  elsetrecslem  49799