Theorem intnand 492

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

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

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 400

This theorem is referenced by:  csbxp  5614  poxp  7805  suppss2  7847  suppco  7853  supp0cosupp0OLD  7856  imacosuppOLD  7858  cfsuc  9668  axunnd  10007  difreicc  12862  fzpreddisj  12951  fzp1nel  12986  repsundef  14124  cshnz  14145  fprodntriv  15288  bitsfzo  15774  bitsmod  15775  gcdnncl  15846  gcd2n0cl  15848  qredeu  15992  cncongr2  16002  divnumden  16078  divdenle  16079  phisum  16117  pythagtriplem4  16146  pythagtriplem8  16150  pythagtriplem9  16151  isnsgrp  17897  isnmnd  17907  mgm2nsgrplem2  18076  0ringnnzr  20035  frlmssuvc2  20484  mamufacex  20996  mavmulsolcl  21156  maducoeval2  21245  opnfbas  22447  lgsneg  25905  numedglnl  26937  umgredgnlp  26940  umgr2edg1  27001  umgr2edgneu  27004  uhgrnbgr0nb  27144  nfrgr2v  28057  4cycl2vnunb  28075  hashxpe  30555  divnumden2  30560  fmlasucdisj  32759  poseq  33208  nodenselem8  33308  unbdqndv1  33960  relowlssretop  34780  relowlpssretop  34781  finxpreclem6  34813  itg2addnclem2  35109  elpadd0  37105  dihatlat  38630  dihjatcclem1  38714  rmspecnonsq  39848  rpnnen3lem  39972  gtnelicc  42137  xrgtnelicc  42175  limcrecl  42271  sumnnodd  42272  jumpncnp  42540  stoweidlem39  42681  stoweidlem59  42701  fourierdlem12  42761  preimagelt  43337  preimalegt  43338  pgrpgt2nabl  44768  lindslinindsimp1  44866  lmod1zrnlvec  44903  rrxsphere  45162