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  5784  poxp  8154  frxp3  8177  poseq  8184  suppss2  8226  suppco  8232  cfsuc  10298  axunnd  10637  difreicc  13525  fzpreddisj  13614  fzp1nel  13652  repsundef  14810  cshnz  14831  fprodntriv  15979  bitsfzo  16473  bitsmod  16474  gcdnncl  16545  gcd2n0cl  16547  qredeu  16696  cncongr2  16706  divnumden  16786  divdenle  16787  phisum  16829  pythagtriplem4  16858  pythagtriplem8  16862  pythagtriplem9  16863  cat1lem  18142  isnsgrp  18737  isnmnd  18752  mgm2nsgrplem2  18933  0ringnnzr  20526  frlmssuvc2  21816  psdmul  22171  mamufacex  22401  mavmulsolcl  22558  maducoeval2  22647  opnfbas  23851  lgsneg  27366  nodenselem8  27737  noinfbnd2lem1  27776  numedglnl  29162  umgredgnlp  29165  umgr2edg1  29229  umgr2edgneu  29232  uhgrnbgr0nb  29372  nfrgr2v  30292  4cycl2vnunb  30310  hashxpe  32812  divnumden2  32818  fmlasucdisj  35405  weiunpo  36467  weiunfr  36469  unbdqndv1  36510  relowlssretop  37365  relowlpssretop  37366  finxpreclem6  37398  itg2addnclem2  37680  elpadd0  39812  dihatlat  41337  dihjatcclem1  41421  aks4d1p8d1  42086  sticksstones22  42170  rmspecnonsq  42923  rpnnen3lem  43048  tfsconcatb0  43362  rexanuz2nf  45508  gtnelicc  45518  xrgtnelicc  45556  limcrecl  45649  sumnnodd  45650  jumpncnp  45918  stoweidlem39  46059  stoweidlem59  46079  fourierdlem12  46139  preimagelt  46719  preimalegt  46720  pgrpgt2nabl  48287  lindslinindsimp1  48379  lmod1zrnlvec  48416  rrxsphere  48674