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  5723  poxp  8068  frxp3  8091  poseq  8098  suppss2  8140  suppco  8146  cfsuc  10165  axunnd  10505  difreicc  13398  fzpreddisj  13487  fzp1nel  13525  repsundef  14692  cshnz  14713  fprodntriv  15863  bitsfzo  16360  bitsmod  16361  gcdnncl  16432  gcd2n0cl  16434  qredeu  16583  cncongr2  16593  divnumden  16673  divdenle  16674  phisum  16716  pythagtriplem4  16745  pythagtriplem8  16749  pythagtriplem9  16750  cat1lem  18018  isnsgrp  18646  isnmnd  18661  mgm2nsgrplem2  18842  0ringnnzr  20456  frlmssuvc2  21748  psdmul  22107  mamufacex  22338  mavmulsolcl  22493  maducoeval2  22582  opnfbas  23784  lgsneg  27286  nodenselem8  27657  noinfbnd2lem1  27696  pw2cut2  28419  numedglnl  29166  umgredgnlp  29169  umgr2edg1  29233  umgr2edgneu  29236  uhgrnbgr0nb  29376  nfrgr2v  30296  4cycl2vnunb  30314  hashxpe  32836  elq2  32841  divnumden2  32845  esplyfval3  33679  fmlasucdisj  35542  weiunpo  36608  weiunfr  36610  unbdqndv1  36651  relowlssretop  37507  relowlpssretop  37508  finxpreclem6  37540  itg2addnclem2  37812  elpadd0  40008  dihatlat  41533  dihjatcclem1  41617  aks4d1p8d1  42277  sticksstones22  42361  rmspecnonsq  43091  rpnnen3lem  43215  tfsconcatb0  43528  rexanuz2nf  45678  gtnelicc  45688  xrgtnelicc  45726  limcrecl  45817  sumnnodd  45818  jumpncnp  46084  stoweidlem39  46225  stoweidlem59  46245  fourierdlem12  46305  preimagelt  46885  preimalegt  46886  pgrpgt2nabl  48554  lindslinindsimp1  48645  lmod1zrnlvec  48682  rrxsphere  48936