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  5799  poxp  8169  frxp3  8192  poseq  8199  suppss2  8241  suppco  8247  cfsuc  10326  axunnd  10665  difreicc  13544  fzpreddisj  13633  fzp1nel  13668  repsundef  14819  cshnz  14840  fprodntriv  15990  bitsfzo  16481  bitsmod  16482  gcdnncl  16553  gcd2n0cl  16555  qredeu  16705  cncongr2  16715  divnumden  16795  divdenle  16796  phisum  16837  pythagtriplem4  16866  pythagtriplem8  16870  pythagtriplem9  16871  cat1lem  18163  isnsgrp  18761  isnmnd  18776  mgm2nsgrplem2  18954  0ringnnzr  20551  frlmssuvc2  21838  psdmul  22193  mamufacex  22421  mavmulsolcl  22578  maducoeval2  22667  opnfbas  23871  lgsneg  27383  nodenselem8  27754  noinfbnd2lem1  27793  numedglnl  29179  umgredgnlp  29182  umgr2edg1  29246  umgr2edgneu  29249  uhgrnbgr0nb  29389  nfrgr2v  30304  4cycl2vnunb  30322  hashxpe  32814  divnumden2  32819  fmlasucdisj  35367  weiunpo  36431  weiunfr  36433  unbdqndv1  36474  relowlssretop  37329  relowlpssretop  37330  finxpreclem6  37362  itg2addnclem2  37632  elpadd0  39766  dihatlat  41291  dihjatcclem1  41375  aks4d1p8d1  42041  sticksstones22  42125  rmspecnonsq  42863  rpnnen3lem  42988  tfsconcatb0  43306  rexanuz2nf  45408  gtnelicc  45418  xrgtnelicc  45456  limcrecl  45550  sumnnodd  45551  jumpncnp  45819  stoweidlem39  45960  stoweidlem59  45980  fourierdlem12  46040  preimagelt  46620  preimalegt  46621  pgrpgt2nabl  48091  lindslinindsimp1  48186  lmod1zrnlvec  48223  rrxsphere  48482