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  5730  poxp  8084  frxp3  8107  poseq  8114  suppss2  8156  suppco  8162  cfsuc  10186  axunnd  10525  difreicc  13421  fzpreddisj  13510  fzp1nel  13548  repsundef  14712  cshnz  14733  fprodntriv  15884  bitsfzo  16381  bitsmod  16382  gcdnncl  16453  gcd2n0cl  16455  qredeu  16604  cncongr2  16614  divnumden  16694  divdenle  16695  phisum  16737  pythagtriplem4  16766  pythagtriplem8  16770  pythagtriplem9  16771  cat1lem  18038  isnsgrp  18632  isnmnd  18647  mgm2nsgrplem2  18828  0ringnnzr  20445  frlmssuvc2  21737  psdmul  22086  mamufacex  22316  mavmulsolcl  22471  maducoeval2  22560  opnfbas  23762  lgsneg  27265  nodenselem8  27636  noinfbnd2lem1  27675  numedglnl  29124  umgredgnlp  29127  umgr2edg1  29191  umgr2edgneu  29194  uhgrnbgr0nb  29334  nfrgr2v  30251  4cycl2vnunb  30269  hashxpe  32782  elq2  32786  divnumden2  32790  fmlasucdisj  35379  weiunpo  36446  weiunfr  36448  unbdqndv1  36489  relowlssretop  37344  relowlpssretop  37345  finxpreclem6  37377  itg2addnclem2  37659  elpadd0  39796  dihatlat  41321  dihjatcclem1  41405  aks4d1p8d1  42065  sticksstones22  42149  rmspecnonsq  42888  rpnnen3lem  43013  tfsconcatb0  43326  rexanuz2nf  45481  gtnelicc  45491  xrgtnelicc  45529  limcrecl  45620  sumnnodd  45621  jumpncnp  45889  stoweidlem39  46030  stoweidlem59  46050  fourierdlem12  46110  preimagelt  46690  preimalegt  46691  pgrpgt2nabl  48347  lindslinindsimp1  48439  lmod1zrnlvec  48476  rrxsphere  48730