Theorem intnand 953

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

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

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 196  df-an 385

This theorem is referenced by:  csbxp  5123  poxp  7176  suppss2  7216  supp0cosupp0  7221  imacosupp  7222  cdadom1  8891  cfsuc  8962  axunnd  9297  difreicc  12175  fzpreddisj  12260  fzp1nel  12293  repsundef  13369  cshnz  13389  fprodntriv  14511  bitsfzo  14995  bitsmod  14996  gcdnncl  15067  gcd2n0cl  15069  qredeu  15210  cncongr2  15220  divnumden  15294  divdenle  15295  phisum  15333  pythagtriplem4  15362  pythagtriplem8  15366  pythagtriplem9  15367  isnsgrp  17111  isnmnd  17121  mgm2nsgrplem2  17229  0ringnnzr  19090  frlmssuvc2  19953  mamufacex  20014  mavmulsolcl  20176  maducoeval2  20265  opnfbas  21456  lgsneg  24846  umgredgnlp  25818  usgra2edg1  25912  nbusgra  25957  cyclnspth  26159  frgra2v  26526  4cycl2vnunb  26544  2spotdisj  26588  2spotmdisj  26595  numclwwlk3lem  26635  divnumden2  28951  poseq  30994  nodenselem8  31087  unbdqndv1  31669  relowlssretop  32387  relowlpssretop  32388  finxpreclem6  32409  itg2addnclem2  32632  elpadd0  34113  dihatlat  35641  dihjatcclem1  35725  rmspecnonsq  36490  rpnnen3lem  36616  gtnelicc  38569  xrgtnelicc  38612  limcrecl  38696  sumnnodd  38697  jumpncnp  38784  stoweidlem39  38932  stoweidlem59  38952  fourierdlem12  39012  preimagelt  39589  preimalegt  39590  umgr2edg1  40438  umgr2edgneu  40441  uhgrnbgr0nb  40576  nfrgr2v  41442  4cycl2vnunb-av  41460  av-numclwwlkffin0  41513  av-numclwwlk3lem  41538  pgrpgt2nabl  41941  lindslinindsimp1  42040  lmod1zrnlvec  42077