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  5788  poxp  8152  frxp3  8175  poseq  8182  suppss2  8224  suppco  8230  cfsuc  10295  axunnd  10634  difreicc  13521  fzpreddisj  13610  fzp1nel  13648  repsundef  14806  cshnz  14827  fprodntriv  15975  bitsfzo  16469  bitsmod  16470  gcdnncl  16541  gcd2n0cl  16543  qredeu  16692  cncongr2  16702  divnumden  16782  divdenle  16783  phisum  16824  pythagtriplem4  16853  pythagtriplem8  16857  pythagtriplem9  16858  cat1lem  18150  isnsgrp  18749  isnmnd  18764  mgm2nsgrplem2  18945  0ringnnzr  20542  frlmssuvc2  21833  psdmul  22188  mamufacex  22416  mavmulsolcl  22573  maducoeval2  22662  opnfbas  23866  lgsneg  27380  nodenselem8  27751  noinfbnd2lem1  27790  numedglnl  29176  umgredgnlp  29179  umgr2edg1  29243  umgr2edgneu  29246  uhgrnbgr0nb  29386  nfrgr2v  30301  4cycl2vnunb  30319  hashxpe  32817  divnumden2  32822  fmlasucdisj  35384  weiunpo  36448  weiunfr  36450  unbdqndv1  36491  relowlssretop  37346  relowlpssretop  37347  finxpreclem6  37379  itg2addnclem2  37659  elpadd0  39792  dihatlat  41317  dihjatcclem1  41401  aks4d1p8d1  42066  sticksstones22  42150  rmspecnonsq  42895  rpnnen3lem  43020  tfsconcatb0  43334  rexanuz2nf  45443  gtnelicc  45453  xrgtnelicc  45491  limcrecl  45585  sumnnodd  45586  jumpncnp  45854  stoweidlem39  45995  stoweidlem59  46015  fourierdlem12  46075  preimagelt  46655  preimalegt  46656  pgrpgt2nabl  48211  lindslinindsimp1  48303  lmod1zrnlvec  48340  rrxsphere  48598