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  5715  poxp  8058  frxp3  8081  poseq  8088  suppss2  8130  suppco  8136  cfsuc  10148  axunnd  10487  difreicc  13384  fzpreddisj  13473  fzp1nel  13511  repsundef  14678  cshnz  14699  fprodntriv  15849  bitsfzo  16346  bitsmod  16347  gcdnncl  16418  gcd2n0cl  16420  qredeu  16569  cncongr2  16579  divnumden  16659  divdenle  16660  phisum  16702  pythagtriplem4  16731  pythagtriplem8  16735  pythagtriplem9  16736  cat1lem  18003  isnsgrp  18631  isnmnd  18646  mgm2nsgrplem2  18827  0ringnnzr  20440  frlmssuvc2  21732  psdmul  22081  mamufacex  22311  mavmulsolcl  22466  maducoeval2  22555  opnfbas  23757  lgsneg  27259  nodenselem8  27630  noinfbnd2lem1  27669  pw2cut2  28382  numedglnl  29122  umgredgnlp  29125  umgr2edg1  29189  umgr2edgneu  29192  uhgrnbgr0nb  29332  nfrgr2v  30252  4cycl2vnunb  30270  hashxpe  32789  elq2  32794  divnumden2  32798  fmlasucdisj  35443  weiunpo  36509  weiunfr  36511  unbdqndv1  36552  relowlssretop  37407  relowlpssretop  37408  finxpreclem6  37440  itg2addnclem2  37722  elpadd0  39918  dihatlat  41443  dihjatcclem1  41527  aks4d1p8d1  42187  sticksstones22  42271  rmspecnonsq  43010  rpnnen3lem  43134  tfsconcatb0  43447  rexanuz2nf  45600  gtnelicc  45610  xrgtnelicc  45648  limcrecl  45739  sumnnodd  45740  jumpncnp  46006  stoweidlem39  46147  stoweidlem59  46167  fourierdlem12  46227  preimagelt  46807  preimalegt  46808  pgrpgt2nabl  48476  lindslinindsimp1  48568  lmod1zrnlvec  48605  rrxsphere  48859