Theorem intnand 494

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  csbxp  5764  poxp  8130  frxp3  8153  poseq  8160  suppss2  8202  suppco  8208  cfsuc  10256  axunnd  10598  difreicc  13529  fzpreddisj  13620  fzp1nel  13658  repsundef  14834  cshnz  14855  fprodntriv  16021  bitsfzo  16517  bitsmod  16518  gcdnncl  16589  gcd2n0cl  16591  qredeu  16740  cncongr2  16750  divnumden  16831  divdenle  16832  phisum  16874  pythagtriplem4  16903  pythagtriplem8  16907  pythagtriplem9  16908  cat1lem  18177  isnsgrp  18815  isnmnd  18830  mgm2nsgrplem2  19020  0ringnnzr  20675  frlmssuvc2  21997  psdmul  22381  mamufacex  22605  mavmulsolcl  22760  maducoeval2  22849  opnfbas  24052  lgsneg  27538  nodenselem8  27908  noinfbnd2lem1  27947  pw2cut2  28708  numedglnl  29551  umgredgnlp  29554  umgr2edg1  29621  umgr2edgneu  29624  uhgrnbgr0nb  29764  nfrgr2v  30696  4cycl2vnunb  30714  hashxpe  33224  elq2  33228  divnumden2  33232  esplyfval3  34028  fmlasucdisj  35930  nmulprop  36721  weiunpo  37035  weiunfr  37037  unbdqndv1  37156  relowlssretop  38068  relowlpssretop  38069  finxpreclem6  38101  itg2addnclem2  38382  elpadd0  40643  dihatlat  42168  dihjatcclem1  42252  aks4d1p8d1  42911  sticksstones22  42995  rmspecnonsq  43694  rpnnen3lem  43818  tfsconcatb0  44131  rexanuz2nf  46266  gtnelicc  46276  xrgtnelicc  46314  limcrecl  46405  sumnnodd  46406  jumpncnp  46672  stoweidlem39  46813  stoweidlem59  46833  fourierdlem12  46893  preimagelt  47473  preimalegt  47474  pgrpgt2nabl  49205  lindslinindsimp1  49296  lmod1zrnlvec  49333  rrxsphere  49587