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

This theorem is referenced by:  csbxp  5684  poxp  7953  suppss2  8000  suppco  8006  cfsuc  9997  axunnd  10336  difreicc  13198  fzpreddisj  13287  fzp1nel  13322  repsundef  14465  cshnz  14486  fprodntriv  15633  bitsfzo  16123  bitsmod  16124  gcdnncl  16195  gcd2n0cl  16197  qredeu  16344  cncongr2  16354  divnumden  16433  divdenle  16434  phisum  16472  pythagtriplem4  16501  pythagtriplem8  16505  pythagtriplem9  16506  cat1lem  17792  isnsgrp  18360  isnmnd  18370  mgm2nsgrplem2  18539  0ringnnzr  20521  frlmssuvc2  20983  mamufacex  21519  mavmulsolcl  21681  maducoeval2  21770  opnfbas  22974  lgsneg  26450  numedglnl  27495  umgredgnlp  27498  umgr2edg1  27559  umgr2edgneu  27562  uhgrnbgr0nb  27702  nfrgr2v  28615  4cycl2vnunb  28633  hashxpe  31106  divnumden2  31111  fmlasucdisj  33340  frxp3  33776  poseq  33781  nodenselem8  33873  noinfbnd2lem1  33912  unbdqndv1  34667  relowlssretop  35513  relowlpssretop  35514  finxpreclem6  35546  itg2addnclem2  35808  elpadd0  37802  dihatlat  39327  dihjatcclem1  39411  aks4d1p8d1  40072  sticksstones22  40104  rmspecnonsq  40709  rpnnen3lem  40833  gtnelicc  42992  xrgtnelicc  43030  limcrecl  43124  sumnnodd  43125  jumpncnp  43393  stoweidlem39  43534  stoweidlem59  43554  fourierdlem12  43614  preimagelt  44190  preimalegt  44191  pgrpgt2nabl  45654  lindslinindsimp1  45750  lmod1zrnlvec  45787  rrxsphere  46046