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  5740  poxp  8109  frxp3  8132  poseq  8139  suppss2  8181  suppco  8187  cfsuc  10216  axunnd  10555  difreicc  13451  fzpreddisj  13540  fzp1nel  13578  repsundef  14742  cshnz  14763  fprodntriv  15914  bitsfzo  16411  bitsmod  16412  gcdnncl  16483  gcd2n0cl  16485  qredeu  16634  cncongr2  16644  divnumden  16724  divdenle  16725  phisum  16767  pythagtriplem4  16796  pythagtriplem8  16800  pythagtriplem9  16801  cat1lem  18064  isnsgrp  18656  isnmnd  18671  mgm2nsgrplem2  18852  0ringnnzr  20440  frlmssuvc2  21710  psdmul  22059  mamufacex  22289  mavmulsolcl  22444  maducoeval2  22533  opnfbas  23735  lgsneg  27238  nodenselem8  27609  noinfbnd2lem1  27648  numedglnl  29077  umgredgnlp  29080  umgr2edg1  29144  umgr2edgneu  29147  uhgrnbgr0nb  29287  nfrgr2v  30207  4cycl2vnunb  30225  hashxpe  32738  elq2  32742  divnumden2  32746  fmlasucdisj  35386  weiunpo  36448  weiunfr  36450  unbdqndv1  36491  relowlssretop  37346  relowlpssretop  37347  finxpreclem6  37379  itg2addnclem2  37661  elpadd0  39798  dihatlat  41323  dihjatcclem1  41407  aks4d1p8d1  42067  sticksstones22  42151  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  48344  lindslinindsimp1  48436  lmod1zrnlvec  48473  rrxsphere  48727