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  5725  poxp  8070  frxp3  8093  poseq  8100  suppss2  8142  suppco  8148  cfsuc  10169  axunnd  10509  difreicc  13402  fzpreddisj  13491  fzp1nel  13529  repsundef  14696  cshnz  14717  fprodntriv  15867  bitsfzo  16364  bitsmod  16365  gcdnncl  16436  gcd2n0cl  16438  qredeu  16587  cncongr2  16597  divnumden  16677  divdenle  16678  phisum  16720  pythagtriplem4  16749  pythagtriplem8  16753  pythagtriplem9  16754  cat1lem  18022  isnsgrp  18650  isnmnd  18665  mgm2nsgrplem2  18846  0ringnnzr  20460  frlmssuvc2  21752  psdmul  22111  mamufacex  22342  mavmulsolcl  22497  maducoeval2  22586  opnfbas  23788  lgsneg  27290  nodenselem8  27661  noinfbnd2lem1  27700  pw2cut2  28460  numedglnl  29219  umgredgnlp  29222  umgr2edg1  29286  umgr2edgneu  29289  uhgrnbgr0nb  29429  nfrgr2v  30349  4cycl2vnunb  30367  hashxpe  32889  elq2  32894  divnumden2  32898  esplyfval3  33732  fmlasucdisj  35595  weiunpo  36661  weiunfr  36663  unbdqndv1  36710  relowlssretop  37570  relowlpssretop  37571  finxpreclem6  37603  itg2addnclem2  37875  elpadd0  40091  dihatlat  41616  dihjatcclem1  41700  aks4d1p8d1  42360  sticksstones22  42444  rmspecnonsq  43170  rpnnen3lem  43294  tfsconcatb0  43607  rexanuz2nf  45757  gtnelicc  45767  xrgtnelicc  45805  limcrecl  45896  sumnnodd  45897  jumpncnp  46163  stoweidlem39  46304  stoweidlem59  46324  fourierdlem12  46384  preimagelt  46964  preimalegt  46965  pgrpgt2nabl  48633  lindslinindsimp1  48724  lmod1zrnlvec  48761  rrxsphere  49015