Theorem intnand 489

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

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

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 206  df-an 397

This theorem is referenced by:  csbxp  5775  poxp  8116  frxp3  8139  poseq  8146  suppss2  8187  suppco  8193  cfsuc  10254  axunnd  10593  difreicc  13465  fzpreddisj  13554  fzp1nel  13589  repsundef  14725  cshnz  14746  fprodntriv  15890  bitsfzo  16380  bitsmod  16381  gcdnncl  16452  gcd2n0cl  16454  qredeu  16599  cncongr2  16609  divnumden  16688  divdenle  16689  phisum  16727  pythagtriplem4  16756  pythagtriplem8  16760  pythagtriplem9  16761  cat1lem  18050  isnsgrp  18648  isnmnd  18663  mgm2nsgrplem2  18836  0ringnnzr  20414  frlmssuvc2  21569  mamufacex  22111  mavmulsolcl  22273  maducoeval2  22362  opnfbas  23566  lgsneg  27048  nodenselem8  27418  noinfbnd2lem1  27457  numedglnl  28659  umgredgnlp  28662  umgr2edg1  28723  umgr2edgneu  28726  uhgrnbgr0nb  28866  nfrgr2v  29780  4cycl2vnunb  29798  hashxpe  32274  divnumden2  32279  fmlasucdisj  34676  unbdqndv1  35687  relowlssretop  36547  relowlpssretop  36548  finxpreclem6  36580  itg2addnclem2  36843  elpadd0  38983  dihatlat  40508  dihjatcclem1  40592  aks4d1p8d1  41255  sticksstones22  41290  rmspecnonsq  41947  rpnnen3lem  42072  tfsconcatb0  42396  rexanuz2nf  44502  gtnelicc  44512  xrgtnelicc  44550  limcrecl  44644  sumnnodd  44645  jumpncnp  44913  stoweidlem39  45054  stoweidlem59  45074  fourierdlem12  45134  preimagelt  45714  preimalegt  45715  pgrpgt2nabl  47131  lindslinindsimp1  47226  lmod1zrnlvec  47263  rrxsphere  47522