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  5756  poxp  8150  frxp3  8178  poseq  8185  suppss2  8228  suppco  8234  cfsuc  10345  axunnd  10691  difreicc  13625  fzpreddisj  13717  fzp1nel  13755  repsundef  14933  cshnz  14954  fprodntriv  16121  bitsfzo  16617  bitsmod  16618  gcdnncl  16689  gcd2n0cl  16691  qredeu  16845  cncongr2  16855  divnumden  16936  divdenle  16937  phisum  16980  pythagtriplem4  17009  pythagtriplem8  17013  pythagtriplem9  17014  cat1lem  18283  isnsgrp  18924  isnmnd  18939  mgm2nsgrplem2  19130  0ringnnzr  20788  frlmssuvc2  22113  psdmul  22499  mamufacex  22723  mavmulsolcl  22878  maducoeval2  22967  opnfbas  24173  lgsneg  27660  nodenselem8  28060  noinfbnd2lem1  28099  pw2cut2  28860  numedglnl  29734  umgredgnlp  29737  umgr2edg1  29804  umgr2edgneu  29807  uhgrnbgr0nb  29947  nfrgr2v  30885  4cycl2vnunb  30903  hashxpe  33452  elq2  33456  divnumden2  33460  esplyfval3  34257  maxssj0  35960  fmlasucdisj  36285  nmulprop  37066  weiunpo  37380  weiunfr  37382  unbdqndv1  37501  relowlssretop  38426  relowlpssretop  38427  finxpreclem6  38459  itg2addnclem2  38730  elpadd0  41006  dihatlat  42531  dihjatcclem1  42615  aks4d1p8d1  43274  sticksstones22  43358  rmspecnonsq  44054  rpnnen3lem  44178  tfsconcatb0  44486  rexanuz2nf  46641  gtnelicc  46651  xrgtnelicc  46689  limcrecl  46780  sumnnodd  46781  jumpncnp  47047  stoweidlem39  47188  stoweidlem59  47208  fourierdlem12  47268  preimagelt  47848  preimalegt  47849  pgrpgt2nabl  49617  lindslinindsimp1  49708  lmod1zrnlvec  49745  rrxsphere  49999