Theorem intnand 487

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

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

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 206  df-an 395

This theorem is referenced by:  csbxp  5776  poxp  8131  frxp3  8154  poseq  8161  suppss2  8204  suppco  8210  cfsuc  10280  axunnd  10619  difreicc  13493  fzpreddisj  13582  fzp1nel  13617  repsundef  14753  cshnz  14774  fprodntriv  15918  bitsfzo  16409  bitsmod  16410  gcdnncl  16481  gcd2n0cl  16483  qredeu  16628  cncongr2  16638  divnumden  16719  divdenle  16720  phisum  16758  pythagtriplem4  16787  pythagtriplem8  16791  pythagtriplem9  16792  cat1lem  18084  isnsgrp  18682  isnmnd  18697  mgm2nsgrplem2  18875  0ringnnzr  20466  frlmssuvc2  21733  psdmul  22098  mamufacex  22326  mavmulsolcl  22483  maducoeval2  22572  opnfbas  23776  lgsneg  27284  nodenselem8  27654  noinfbnd2lem1  27693  numedglnl  29013  umgredgnlp  29016  umgr2edg1  29080  umgr2edgneu  29083  uhgrnbgr0nb  29223  nfrgr2v  30138  4cycl2vnunb  30156  hashxpe  32633  divnumden2  32638  fmlasucdisj  35079  unbdqndv1  36053  relowlssretop  36912  relowlpssretop  36913  finxpreclem6  36945  itg2addnclem2  37215  elpadd0  39351  dihatlat  40876  dihjatcclem1  40960  aks4d1p8d1  41624  sticksstones22  41709  rmspecnonsq  42392  rpnnen3lem  42517  tfsconcatb0  42838  rexanuz2nf  44938  gtnelicc  44948  xrgtnelicc  44986  limcrecl  45080  sumnnodd  45081  jumpncnp  45349  stoweidlem39  45490  stoweidlem59  45510  fourierdlem12  45570  preimagelt  46150  preimalegt  46151  pgrpgt2nabl  47542  lindslinindsimp1  47637  lmod1zrnlvec  47674  rrxsphere  47933