Theorem intnand 494

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  csbxp  5756  poxp  8127  frxp3  8150  poseq  8157  suppss2  8199  suppco  8205  cfsuc  10262  axunnd  10608  difreicc  13540  fzpreddisj  13631  fzp1nel  13669  repsundef  14845  cshnz  14866  fprodntriv  16032  bitsfzo  16528  bitsmod  16529  gcdnncl  16600  gcd2n0cl  16602  qredeu  16751  cncongr2  16761  divnumden  16842  divdenle  16843  phisum  16885  pythagtriplem4  16914  pythagtriplem8  16918  pythagtriplem9  16919  cat1lem  18188  isnsgrp  18828  isnmnd  18843  mgm2nsgrplem2  19034  0ringnnzr  20689  frlmssuvc2  22011  psdmul  22397  mamufacex  22621  mavmulsolcl  22776  maducoeval2  22865  opnfbas  24071  lgsneg  27560  nodenselem8  27930  noinfbnd2lem1  27969  pw2cut2  28730  numedglnl  29604  umgredgnlp  29607  umgr2edg1  29674  umgr2edgneu  29677  uhgrnbgr0nb  29817  nfrgr2v  30755  4cycl2vnunb  30773  hashxpe  33281  elq2  33285  divnumden2  33289  esplyfval3  34085  fmlasucdisj  35981  nmulprop  36773  weiunpo  37087  weiunfr  37089  unbdqndv1  37208  relowlssretop  38120  relowlpssretop  38121  finxpreclem6  38153  itg2addnclem2  38424  elpadd0  40685  dihatlat  42210  dihjatcclem1  42294  aks4d1p8d1  42953  sticksstones22  43037  rmspecnonsq  43751  rpnnen3lem  43875  tfsconcatb0  44188  rexanuz2nf  46323  gtnelicc  46333  xrgtnelicc  46371  limcrecl  46462  sumnnodd  46463  jumpncnp  46729  stoweidlem39  46870  stoweidlem59  46890  fourierdlem12  46950  preimagelt  47530  preimalegt  47531  pgrpgt2nabl  49299  lindslinindsimp1  49390  lmod1zrnlvec  49427  rrxsphere  49681