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  5752  poxp  8140  frxp3  8168  poseq  8175  suppss2  8217  suppco  8223  cfsuc  10335  axunnd  10681  difreicc  13615  fzpreddisj  13707  fzp1nel  13745  repsundef  14922  cshnz  14943  fprodntriv  16109  bitsfzo  16605  bitsmod  16606  gcdnncl  16677  gcd2n0cl  16679  qredeu  16833  cncongr2  16843  divnumden  16924  divdenle  16925  phisum  16968  pythagtriplem4  16997  pythagtriplem8  17001  pythagtriplem9  17002  cat1lem  18271  isnsgrp  18912  isnmnd  18927  mgm2nsgrplem2  19118  0ringnnzr  20776  frlmssuvc2  22101  psdmul  22487  mamufacex  22711  mavmulsolcl  22866  maducoeval2  22955  opnfbas  24161  lgsneg  27648  nodenselem8  28048  noinfbnd2lem1  28087  pw2cut2  28848  numedglnl  29722  umgredgnlp  29725  umgr2edg1  29792  umgr2edgneu  29795  uhgrnbgr0nb  29935  nfrgr2v  30873  4cycl2vnunb  30891  hashxpe  33399  elq2  33403  divnumden2  33407  esplyfval3  34204  fmlasucdisj  36164  nmulprop  36939  weiunpo  37253  weiunfr  37255  unbdqndv1  37374  relowlssretop  38286  relowlpssretop  38287  finxpreclem6  38319  itg2addnclem2  38590  elpadd0  40866  dihatlat  42391  dihjatcclem1  42475  aks4d1p8d1  43134  sticksstones22  43218  rmspecnonsq  43913  rpnnen3lem  44037  tfsconcatb0  44345  rexanuz2nf  46501  gtnelicc  46511  xrgtnelicc  46549  limcrecl  46640  sumnnodd  46641  jumpncnp  46907  stoweidlem39  47048  stoweidlem59  47068  fourierdlem12  47128  preimagelt  47708  preimalegt  47709  pgrpgt2nabl  49477  lindslinindsimp1  49568  lmod1zrnlvec  49605  rrxsphere  49859