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  5732  poxp  8078  frxp3  8101  poseq  8108  suppss2  8150  suppco  8156  cfsuc  10179  axunnd  10519  difreicc  13437  fzpreddisj  13527  fzp1nel  13565  repsundef  14733  cshnz  14754  fprodntriv  15907  bitsfzo  16404  bitsmod  16405  gcdnncl  16476  gcd2n0cl  16478  qredeu  16627  cncongr2  16637  divnumden  16718  divdenle  16719  phisum  16761  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  cat1lem  18063  isnsgrp  18691  isnmnd  18706  mgm2nsgrplem2  18890  0ringnnzr  20502  frlmssuvc2  21775  psdmul  22132  mamufacex  22361  mavmulsolcl  22516  maducoeval2  22605  opnfbas  23807  lgsneg  27284  nodenselem8  27655  noinfbnd2lem1  27694  pw2cut2  28454  numedglnl  29213  umgredgnlp  29216  umgr2edg1  29280  umgr2edgneu  29283  uhgrnbgr0nb  29423  nfrgr2v  30342  4cycl2vnunb  30360  hashxpe  32880  elq2  32885  divnumden2  32889  esplyfval3  33716  fmlasucdisj  35581  weiunpo  36647  weiunfr  36649  unbdqndv1  36768  relowlssretop  37679  relowlpssretop  37680  finxpreclem6  37712  itg2addnclem2  37993  elpadd0  40255  dihatlat  41780  dihjatcclem1  41864  aks4d1p8d1  42523  sticksstones22  42607  rmspecnonsq  43335  rpnnen3lem  43459  tfsconcatb0  43772  rexanuz2nf  45920  gtnelicc  45930  xrgtnelicc  45968  limcrecl  46059  sumnnodd  46060  jumpncnp  46326  stoweidlem39  46467  stoweidlem59  46487  fourierdlem12  46547  preimagelt  47127  preimalegt  47128  pgrpgt2nabl  48842  lindslinindsimp1  48933  lmod1zrnlvec  48970  rrxsphere  49224