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  1479  intn3an2d  1480  intn3an3d  1481  nsb  2106  necon3ai  2971  pssn2lp  4127  sotrieq  5638  ordnbtwn  6488  funun  6624  canth  7401  0mpo0  7533  dfwe2  7809  opabn1stprc  8099  pwuninel2  8315  frrlem11  8337  frrlem12  8338  swoer  8794  swoord1  8795  swoord2  8796  php2OLD  9286  phpeqdOLD  9288  1sdom2dom  9310  en3lp  9683  cantnfp1lem1  9747  cantnfp1lem3  9749  cantnflem2  9759  rankxpsuc  9951  cardmin2  10068  infxpenlem  10082  cardaleph  10158  isfin4p1  10384  fin23lem24  10391  fin23lem25  10393  fin23lem26  10394  fin23lem38  10418  isfin32i  10434  fin34  10459  fin67  10464  nd3  10658  fpwwe2lem12  10711  canthnum  10718  canthwe  10720  pwfseq  10733  gchdjuidm  10737  gchxpidm  10738  r1wunlim  10806  suplem2pr  11122  elnnz  12649  fzneuz  13665  fzodisj  13750  fzodisjsn  13754  hasheq0  14412  swrd0  14706  cnpart  15289  sqreulem  15408  rlimuni  15596  rlimcld2  15624  divalglem6  16446  bitsf1  16492  infpnlem1  16957  ramubcl  17065  ressress  17307  mreexmrid  17701  gsum2d  20014  dprddomprc  20044  ablfacrplem  20109  trivnsimpgd  20141  ablsimpnosubgd  20148  zrninitoringc  20698  rng1nfld  20802  mplsubrglem  22047  mdetunilem6  22644  mdetunilem9  22647  madugsum  22670  infil  23892  fbasfip  23897  fgcl  23907  fin1aufil  23961  hauspwpwf1  24016  ovolicc2lem4  25574  ovolioo  25622  i1fima2sn  25734  itg1addlem4  25753  itg1addlem4OLD  25754  itgsplitioo  25893  lhop1lem  26072  chordthmlem  26893  ressatans  26995  ftalem5  27138  ppiprm  27212  chtprm  27214  lgsdir2lem2  27388  dirith2  27590  noresle  27760  noetasuplem4  27799  noetainflem4  27803  elnnzs  28405  axlowdimlem13  28987  axlowdim1  28992  nfrgr2v  30304  ply1annnr  33696  inelpisys  34118  eulerpartlemgvv  34341  ballotlemfp1  34456  ballotlem4  34463  ballotlemirc  34496  erdszelem8  35166  bccolsum  35701  nn0prpwlem  36288  nn0prpw  36289  ivthALT  36301  nandsym1  36388  onsucsuccmpi  36409  onint1  36415  weiunpo  36431  bj-fununsn1  37219  bj-fvmptunsn1  37223  topdifinffinlem  37313  relowlssretop  37329  domalom  37370  fin2solem  37566  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem26  37606  poimirlem31  37611  mblfinlem1  37617  mblfinlem2  37618  dvasin  37664  dvacos  37665  areacirclem4  37671  ax10fromc7  38851  hdmaplem1  41728  hdmaplem2N  41729  hdmaplem3  41730  negn0nposznnd  42271  fimgmcyc  42489  irrapx1  42784  limnsuc  43227  gneispace  44096  mnuprdlem2  44242  sineq0ALT  44908  sumnnodd  45551  fperdvper  45840  stoweidlem35  45956  stirlinglem5  45999  fourierdlem68  46095  fourierswlem  46151  fouriersw  46152  iundjiunlem  46380  smfmbfcex  46681  et-ltneverrefl  46792  et-sqrtnegnre  46794  singoutnupword  46802  tworepnotupword  46805  requad1  47496  requad2  47497  lmod1zrnlvec  48223  elsetrecslem  48791