Theorem intnand 488

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
intnand	⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Proof of Theorem intnand

Step	Hyp	Ref	Expression
1		intnand.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		simpr 484	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 140	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  csbxp  5719  poxp  8061  frxp3  8084  poseq  8091  suppss2  8133  suppco  8139  cfsuc  10151  axunnd  10490  difreicc  13387  fzpreddisj  13476  fzp1nel  13514  repsundef  14677  cshnz  14698  fprodntriv  15849  bitsfzo  16346  bitsmod  16347  gcdnncl  16418  gcd2n0cl  16420  qredeu  16569  cncongr2  16579  divnumden  16659  divdenle  16660  phisum  16702  pythagtriplem4  16731  pythagtriplem8  16735  pythagtriplem9  16736  cat1lem  18003  isnsgrp  18597  isnmnd  18612  mgm2nsgrplem2  18793  0ringnnzr  20410  frlmssuvc2  21702  psdmul  22051  mamufacex  22281  mavmulsolcl  22436  maducoeval2  22525  opnfbas  23727  lgsneg  27230  nodenselem8  27601  noinfbnd2lem1  27640  numedglnl  29089  umgredgnlp  29092  umgr2edg1  29156  umgr2edgneu  29159  uhgrnbgr0nb  29299  nfrgr2v  30216  4cycl2vnunb  30234  hashxpe  32753  elq2  32757  divnumden2  32761  fmlasucdisj  35382  weiunpo  36449  weiunfr  36451  unbdqndv1  36492  relowlssretop  37347  relowlpssretop  37348  finxpreclem6  37380  itg2addnclem2  37662  elpadd0  39798  dihatlat  41323  dihjatcclem1  41407  aks4d1p8d1  42067  sticksstones22  42151  rmspecnonsq  42890  rpnnen3lem  43014  tfsconcatb0  43327  rexanuz2nf  45481  gtnelicc  45491  xrgtnelicc  45529  limcrecl  45620  sumnnodd  45621  jumpncnp  45889  stoweidlem39  46030  stoweidlem59  46050  fourierdlem12  46110  preimagelt  46690  preimalegt  46691  pgrpgt2nabl  48360  lindslinindsimp1  48452  lmod1zrnlvec  48489  rrxsphere  48743