Theorem intnand 493

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 489	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 141	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  csbxp  5762  poxp  8120  frxp3  8143  poseq  8150  suppss2  8192  suppco  8198  cfsuc  10236  axunnd  10576  difreicc  13506  fzpreddisj  13597  fzp1nel  13635  repsundef  14804  cshnz  14825  fprodntriv  15992  bitsfzo  16488  bitsmod  16489  gcdnncl  16560  gcd2n0cl  16562  qredeu  16711  cncongr2  16721  divnumden  16802  divdenle  16803  phisum  16845  pythagtriplem4  16874  pythagtriplem8  16878  pythagtriplem9  16879  cat1lem  18148  isnsgrp  18776  isnmnd  18791  mgm2nsgrplem2  18976  0ringnnzr  20623  frlmssuvc2  21945  psdmul  22329  mamufacex  22553  mavmulsolcl  22708  maducoeval2  22797  opnfbas  23999  lgsneg  27485  nodenselem8  27855  noinfbnd2lem1  27894  pw2cut2  28655  numedglnl  29494  umgredgnlp  29497  umgr2edg1  29561  umgr2edgneu  29564  uhgrnbgr0nb  29704  nfrgr2v  30623  4cycl2vnunb  30641  hashxpe  33152  elq2  33156  divnumden2  33160  esplyfval3  33962  fmlasucdisj  35891  nmulprop  36682  weiunpo  36996  weiunfr  36998  unbdqndv1  37117  relowlssretop  38029  relowlpssretop  38030  finxpreclem6  38062  itg2addnclem2  38343  elpadd0  40603  dihatlat  42128  dihjatcclem1  42212  aks4d1p8d1  42871  sticksstones22  42955  rmspecnonsq  43654  rpnnen3lem  43778  tfsconcatb0  44091  rexanuz2nf  46226  gtnelicc  46236  xrgtnelicc  46274  limcrecl  46365  sumnnodd  46366  jumpncnp  46632  stoweidlem39  46773  stoweidlem59  46793  fourierdlem12  46853  preimagelt  47433  preimalegt  47434  pgrpgt2nabl  49166  lindslinindsimp1  49257  lmod1zrnlvec  49294  rrxsphere  49548