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  5733  poxp  8080  frxp3  8103  poseq  8110  suppss2  8152  suppco  8158  cfsuc  10179  axunnd  10519  difreicc  13412  fzpreddisj  13501  fzp1nel  13539  repsundef  14706  cshnz  14727  fprodntriv  15877  bitsfzo  16374  bitsmod  16375  gcdnncl  16446  gcd2n0cl  16448  qredeu  16597  cncongr2  16607  divnumden  16687  divdenle  16688  phisum  16730  pythagtriplem4  16759  pythagtriplem8  16763  pythagtriplem9  16764  cat1lem  18032  isnsgrp  18660  isnmnd  18675  mgm2nsgrplem2  18859  0ringnnzr  20473  frlmssuvc2  21765  psdmul  22124  mamufacex  22355  mavmulsolcl  22510  maducoeval2  22599  opnfbas  23801  lgsneg  27303  nodenselem8  27674  noinfbnd2lem1  27713  pw2cut2  28473  numedglnl  29233  umgredgnlp  29236  umgr2edg1  29300  umgr2edgneu  29303  uhgrnbgr0nb  29443  nfrgr2v  30363  4cycl2vnunb  30381  hashxpe  32902  elq2  32907  divnumden2  32911  esplyfval3  33753  fmlasucdisj  35619  weiunpo  36685  weiunfr  36687  unbdqndv1  36734  relowlssretop  37622  relowlpssretop  37623  finxpreclem6  37655  itg2addnclem2  37927  elpadd0  40189  dihatlat  41714  dihjatcclem1  41798  aks4d1p8d1  42458  sticksstones22  42542  rmspecnonsq  43268  rpnnen3lem  43392  tfsconcatb0  43705  rexanuz2nf  45854  gtnelicc  45864  xrgtnelicc  45902  limcrecl  45993  sumnnodd  45994  jumpncnp  46260  stoweidlem39  46401  stoweidlem59  46421  fourierdlem12  46481  preimagelt  47061  preimalegt  47062  pgrpgt2nabl  48730  lindslinindsimp1  48821  lmod1zrnlvec  48858  rrxsphere  49112