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  5759  poxp  8132  frxp3  8155  poseq  8162  suppss2  8204  suppco  8210  cfsuc  10276  axunnd  10615  difreicc  13506  fzpreddisj  13595  fzp1nel  13633  repsundef  14794  cshnz  14815  fprodntriv  15963  bitsfzo  16459  bitsmod  16460  gcdnncl  16531  gcd2n0cl  16533  qredeu  16682  cncongr2  16692  divnumden  16772  divdenle  16773  phisum  16815  pythagtriplem4  16844  pythagtriplem8  16848  pythagtriplem9  16849  cat1lem  18114  isnsgrp  18706  isnmnd  18721  mgm2nsgrplem2  18902  0ringnnzr  20490  frlmssuvc2  21760  psdmul  22109  mamufacex  22339  mavmulsolcl  22494  maducoeval2  22583  opnfbas  23785  lgsneg  27289  nodenselem8  27660  noinfbnd2lem1  27699  numedglnl  29128  umgredgnlp  29131  umgr2edg1  29195  umgr2edgneu  29198  uhgrnbgr0nb  29338  nfrgr2v  30258  4cycl2vnunb  30276  hashxpe  32791  elq2  32795  divnumden2  32799  fmlasucdisj  35426  weiunpo  36488  weiunfr  36490  unbdqndv1  36531  relowlssretop  37386  relowlpssretop  37387  finxpreclem6  37419  itg2addnclem2  37701  elpadd0  39833  dihatlat  41358  dihjatcclem1  41442  aks4d1p8d1  42102  sticksstones22  42186  rmspecnonsq  42905  rpnnen3lem  43030  tfsconcatb0  43343  rexanuz2nf  45499  gtnelicc  45509  xrgtnelicc  45547  limcrecl  45638  sumnnodd  45639  jumpncnp  45907  stoweidlem39  46048  stoweidlem59  46068  fourierdlem12  46128  preimagelt  46708  preimalegt  46709  pgrpgt2nabl  48321  lindslinindsimp1  48413  lmod1zrnlvec  48450  rrxsphere  48708