Theorem intnand 489

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

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

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 397

This theorem is referenced by:  csbxp  5775  poxp  8113  frxp3  8136  poseq  8143  suppss2  8184  suppco  8190  cfsuc  10251  axunnd  10590  difreicc  13460  fzpreddisj  13549  fzp1nel  13584  repsundef  14720  cshnz  14741  fprodntriv  15885  bitsfzo  16375  bitsmod  16376  gcdnncl  16447  gcd2n0cl  16449  qredeu  16594  cncongr2  16604  divnumden  16683  divdenle  16684  phisum  16722  pythagtriplem4  16751  pythagtriplem8  16755  pythagtriplem9  16756  cat1lem  18045  isnsgrp  18613  isnmnd  18628  mgm2nsgrplem2  18799  0ringnnzr  20301  frlmssuvc2  21349  mamufacex  21890  mavmulsolcl  22052  maducoeval2  22141  opnfbas  23345  lgsneg  26821  nodenselem8  27191  noinfbnd2lem1  27230  numedglnl  28401  umgredgnlp  28404  umgr2edg1  28465  umgr2edgneu  28468  uhgrnbgr0nb  28608  nfrgr2v  29522  4cycl2vnunb  29540  hashxpe  32014  divnumden2  32019  fmlasucdisj  34385  unbdqndv1  35379  relowlssretop  36239  relowlpssretop  36240  finxpreclem6  36272  itg2addnclem2  36535  elpadd0  38675  dihatlat  40200  dihjatcclem1  40284  aks4d1p8d1  40944  sticksstones22  40979  rmspecnonsq  41635  rpnnen3lem  41760  tfsconcatb0  42084  rexanuz2nf  44193  gtnelicc  44203  xrgtnelicc  44241  limcrecl  44335  sumnnodd  44336  jumpncnp  44604  stoweidlem39  44745  stoweidlem59  44765  fourierdlem12  44825  preimagelt  45405  preimalegt  45406  pgrpgt2nabl  47032  lindslinindsimp1  47128  lmod1zrnlvec  47165  rrxsphere  47424