Theorem intnand 492

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 488	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 140	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

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

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 209  df-an 400

This theorem is referenced by:  csbxp  5748  poxp  8108  frxp3  8131  poseq  8138  suppss2  8180  suppco  8186  cfsuc  10214  axunnd  10554  difreicc  13488  fzpreddisj  13578  fzp1nel  13616  repsundef  14784  cshnz  14805  fprodntriv  15972  bitsfzo  16469  bitsmod  16470  gcdnncl  16541  gcd2n0cl  16543  qredeu  16692  cncongr2  16702  divnumden  16783  divdenle  16784  phisum  16826  pythagtriplem4  16855  pythagtriplem8  16859  pythagtriplem9  16860  cat1lem  18129  isnsgrp  18757  isnmnd  18772  mgm2nsgrplem2  18956  0ringnnzr  20575  frlmssuvc2  21847  psdmul  22231  mamufacex  22456  mavmulsolcl  22611  maducoeval2  22700  opnfbas  23902  lgsneg  27385  nodenselem8  27755  noinfbnd2lem1  27794  pw2cut2  28555  numedglnl  29345  umgredgnlp  29348  umgr2edg1  29412  umgr2edgneu  29415  uhgrnbgr0nb  29555  nfrgr2v  30474  4cycl2vnunb  30492  hashxpe  33009  elq2  33014  divnumden2  33018  esplyfval3  33869  fmlasucdisj  35749  nmulprop  36540  weiunpo  36825  weiunfr  36827  unbdqndv1  36946  relowlssretop  37857  relowlpssretop  37858  finxpreclem6  37890  itg2addnclem2  38171  elpadd0  40433  dihatlat  41958  dihjatcclem1  42042  aks4d1p8d1  42701  sticksstones22  42785  rmspecnonsq  43484  rpnnen3lem  43608  tfsconcatb0  43921  rexanuz2nf  46066  gtnelicc  46076  xrgtnelicc  46114  limcrecl  46205  sumnnodd  46206  jumpncnp  46472  stoweidlem39  46613  stoweidlem59  46633  fourierdlem12  46693  preimagelt  47273  preimalegt  47274  pgrpgt2nabl  48988  lindslinindsimp1  49079  lmod1zrnlvec  49116  rrxsphere  49370