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  5798  poxp  8165  frxp3  8188  poseq  8195  suppss2  8237  suppco  8243  cfsuc  10322  axunnd  10661  difreicc  13540  fzpreddisj  13629  fzp1nel  13664  repsundef  14815  cshnz  14836  fprodntriv  15984  bitsfzo  16475  bitsmod  16476  gcdnncl  16547  gcd2n0cl  16549  qredeu  16699  cncongr2  16709  divnumden  16790  divdenle  16791  phisum  16832  pythagtriplem4  16861  pythagtriplem8  16865  pythagtriplem9  16866  cat1lem  18158  isnsgrp  18756  isnmnd  18771  mgm2nsgrplem2  18949  0ringnnzr  20546  frlmssuvc2  21833  psdmul  22186  mamufacex  22414  mavmulsolcl  22571  maducoeval2  22660  opnfbas  23864  lgsneg  27374  nodenselem8  27745  noinfbnd2lem1  27784  numedglnl  29170  umgredgnlp  29173  umgr2edg1  29237  umgr2edgneu  29240  uhgrnbgr0nb  29380  nfrgr2v  30295  4cycl2vnunb  30313  hashxpe  32806  divnumden2  32811  fmlasucdisj  35359  weiunpo  36377  weiunfrlem2  36380  unbdqndv1  36422  relowlssretop  37277  relowlpssretop  37278  finxpreclem6  37310  itg2addnclem2  37580  elpadd0  39714  dihatlat  41239  dihjatcclem1  41323  aks4d1p8d1  41989  sticksstones22  42073  rmspecnonsq  42800  rpnnen3lem  42925  tfsconcatb0  43246  rexanuz2nf  45342  gtnelicc  45352  xrgtnelicc  45390  limcrecl  45484  sumnnodd  45485  jumpncnp  45753  stoweidlem39  45894  stoweidlem59  45914  fourierdlem12  45974  preimagelt  46554  preimalegt  46555  pgrpgt2nabl  48009  lindslinindsimp1  48104  lmod1zrnlvec  48141  rrxsphere  48400