Theorem intnand 493

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

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

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 210  df-an 401

This theorem is referenced by:  csbxp  5763  poxp  8124  frxp3  8147  poseq  8154  suppss2  8196  suppco  8202  cfsuc  10241  axunnd  10581  difreicc  13511  fzpreddisj  13601  fzp1nel  13639  repsundef  14808  cshnz  14829  fprodntriv  15996  bitsfzo  16493  bitsmod  16494  gcdnncl  16565  gcd2n0cl  16567  qredeu  16716  cncongr2  16726  divnumden  16807  divdenle  16808  phisum  16850  pythagtriplem4  16879  pythagtriplem8  16883  pythagtriplem9  16884  cat1lem  18153  isnsgrp  18781  isnmnd  18796  mgm2nsgrplem2  18981  0ringnnzr  20609  frlmssuvc2  21914  psdmul  22298  mamufacex  22522  mavmulsolcl  22677  maducoeval2  22766  opnfbas  23968  lgsneg  27451  nodenselem8  27821  noinfbnd2lem1  27860  pw2cut2  28621  numedglnl  29435  umgredgnlp  29438  umgr2edg1  29502  umgr2edgneu  29505  uhgrnbgr0nb  29645  nfrgr2v  30564  4cycl2vnunb  30582  hashxpe  33093  elq2  33097  divnumden2  33101  esplyfval3  33907  fmlasucdisj  35790  nmulprop  36581  weiunpo  36865  weiunfr  36867  unbdqndv1  36986  relowlssretop  37897  relowlpssretop  37898  finxpreclem6  37930  itg2addnclem2  38211  elpadd0  40473  dihatlat  41998  dihjatcclem1  42082  aks4d1p8d1  42741  sticksstones22  42825  rmspecnonsq  43526  rpnnen3lem  43650  tfsconcatb0  43963  rexanuz2nf  46098  gtnelicc  46108  xrgtnelicc  46146  limcrecl  46237  sumnnodd  46238  jumpncnp  46504  stoweidlem39  46645  stoweidlem59  46665  fourierdlem12  46725  preimagelt  47305  preimalegt  47306  pgrpgt2nabl  49031  lindslinindsimp1  49122  lmod1zrnlvec  49159  rrxsphere  49413