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  5622  poxp  7849  suppss2  7896  suppco  7902  cfsuc  9758  axunnd  10097  difreicc  12959  fzpreddisj  13048  fzp1nel  13083  repsundef  14223  cshnz  14244  fprodntriv  15389  bitsfzo  15879  bitsmod  15880  gcdnncl  15951  gcd2n0cl  15953  qredeu  16100  cncongr2  16110  divnumden  16189  divdenle  16190  phisum  16228  pythagtriplem4  16257  pythagtriplem8  16261  pythagtriplem9  16262  cat1lem  17469  isnsgrp  18022  isnmnd  18032  mgm2nsgrplem2  18201  0ringnnzr  20162  frlmssuvc2  20612  mamufacex  21143  mavmulsolcl  21303  maducoeval2  21392  opnfbas  22594  lgsneg  26057  numedglnl  27089  umgredgnlp  27092  umgr2edg1  27153  umgr2edgneu  27156  uhgrnbgr0nb  27296  nfrgr2v  28209  4cycl2vnunb  28227  hashxpe  30702  divnumden2  30707  fmlasucdisj  32932  frxp3  33408  poseq  33413  nodenselem8  33535  noinfbnd2lem1  33574  unbdqndv1  34326  relowlssretop  35154  relowlpssretop  35155  finxpreclem6  35187  itg2addnclem2  35449  elpadd0  37443  dihatlat  38968  dihjatcclem1  39052  rmspecnonsq  40293  rpnnen3lem  40417  gtnelicc  42570  xrgtnelicc  42608  limcrecl  42704  sumnnodd  42705  jumpncnp  42973  stoweidlem39  43114  stoweidlem59  43134  fourierdlem12  43194  preimagelt  43770  preimalegt  43771  pgrpgt2nabl  45228  lindslinindsimp1  45324  lmod1zrnlvec  45361  rrxsphere  45620