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 206  df-an 396

This theorem is referenced by:  csbxp  5765  poxp  8108  frxp3  8131  poseq  8138  suppss2  8180  suppco  8186  cfsuc  10247  axunnd  10586  difreicc  13457  fzpreddisj  13546  fzp1nel  13581  repsundef  14717  cshnz  14738  fprodntriv  15882  bitsfzo  16372  bitsmod  16373  gcdnncl  16444  gcd2n0cl  16446  qredeu  16591  cncongr2  16601  divnumden  16680  divdenle  16681  phisum  16719  pythagtriplem4  16748  pythagtriplem8  16752  pythagtriplem9  16753  cat1lem  18045  isnsgrp  18643  isnmnd  18658  mgm2nsgrplem2  18831  0ringnnzr  20410  frlmssuvc2  21650  mamufacex  22201  mavmulsolcl  22363  maducoeval2  22452  opnfbas  23656  lgsneg  27158  nodenselem8  27528  noinfbnd2lem1  27567  numedglnl  28828  umgredgnlp  28831  umgr2edg1  28892  umgr2edgneu  28895  uhgrnbgr0nb  29035  nfrgr2v  29949  4cycl2vnunb  29967  hashxpe  32443  divnumden2  32448  fmlasucdisj  34845  unbdqndv1  35840  relowlssretop  36700  relowlpssretop  36701  finxpreclem6  36733  itg2addnclem2  36996  elpadd0  39136  dihatlat  40661  dihjatcclem1  40745  aks4d1p8d1  41408  sticksstones22  41443  rmspecnonsq  42100  rpnnen3lem  42225  tfsconcatb0  42549  rexanuz2nf  44654  gtnelicc  44664  xrgtnelicc  44702  limcrecl  44796  sumnnodd  44797  jumpncnp  45065  stoweidlem39  45206  stoweidlem59  45226  fourierdlem12  45286  preimagelt  45866  preimalegt  45867  pgrpgt2nabl  47197  lindslinindsimp1  47292  lmod1zrnlvec  47329  rrxsphere  47588