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  5771  poxp  8127  frxp3  8150  poseq  8157  suppss2  8199  suppco  8205  cfsuc  10272  axunnd  10611  difreicc  13485  fzpreddisj  13574  fzp1nel  13609  repsundef  14745  cshnz  14766  fprodntriv  15910  bitsfzo  16401  bitsmod  16402  gcdnncl  16473  gcd2n0cl  16475  qredeu  16620  cncongr2  16630  divnumden  16711  divdenle  16712  phisum  16750  pythagtriplem4  16779  pythagtriplem8  16783  pythagtriplem9  16784  cat1lem  18076  isnsgrp  18674  isnmnd  18689  mgm2nsgrplem2  18862  0ringnnzr  20451  frlmssuvc2  21716  psdmul  22077  mamufacex  22278  mavmulsolcl  22440  maducoeval2  22529  opnfbas  23733  lgsneg  27241  nodenselem8  27611  noinfbnd2lem1  27650  numedglnl  28944  umgredgnlp  28947  umgr2edg1  29011  umgr2edgneu  29014  uhgrnbgr0nb  29154  nfrgr2v  30069  4cycl2vnunb  30087  hashxpe  32560  divnumden2  32563  fmlasucdisj  34945  unbdqndv1  35919  relowlssretop  36778  relowlpssretop  36779  finxpreclem6  36811  itg2addnclem2  37080  elpadd0  39219  dihatlat  40744  dihjatcclem1  40828  aks4d1p8d1  41492  sticksstones22  41572  rmspecnonsq  42249  rpnnen3lem  42374  tfsconcatb0  42696  rexanuz2nf  44798  gtnelicc  44808  xrgtnelicc  44846  limcrecl  44940  sumnnodd  44941  jumpncnp  45209  stoweidlem39  45350  stoweidlem59  45370  fourierdlem12  45430  preimagelt  46010  preimalegt  46011  pgrpgt2nabl  47353  lindslinindsimp1  47448  lmod1zrnlvec  47485  rrxsphere  47744