Theorem intnand 489

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  csbxp  5719  poxp  8068  frxp3  8091  poseq  8098  suppss2  8140  suppco  8146  cfsuc  10170  axunnd  10510  difreicc  13428  fzpreddisj  13518  fzp1nel  13556  repsundef  14724  cshnz  14745  fprodntriv  15898  bitsfzo  16395  bitsmod  16396  gcdnncl  16467  gcd2n0cl  16469  qredeu  16618  cncongr2  16628  divnumden  16709  divdenle  16710  phisum  16752  pythagtriplem4  16781  pythagtriplem8  16785  pythagtriplem9  16786  cat1lem  18054  isnsgrp  18682  isnmnd  18697  mgm2nsgrplem2  18881  0ringnnzr  20497  frlmssuvc2  21770  psdmul  22154  mamufacex  22379  mavmulsolcl  22534  maducoeval2  22623  opnfbas  23825  lgsneg  27302  nodenselem8  27673  noinfbnd2lem1  27712  pw2cut2  28472  numedglnl  29231  umgredgnlp  29234  umgr2edg1  29298  umgr2edgneu  29301  uhgrnbgr0nb  29441  nfrgr2v  30360  4cycl2vnunb  30378  hashxpe  32899  elq2  32904  divnumden2  32908  esplyfval3  33756  fmlasucdisj  35627  weiunpo  36693  weiunfr  36695  unbdqndv1  36814  relowlssretop  37725  relowlpssretop  37726  finxpreclem6  37758  itg2addnclem2  38039  elpadd0  40301  dihatlat  41826  dihjatcclem1  41910  aks4d1p8d1  42569  sticksstones22  42653  rmspecnonsq  43352  rpnnen3lem  43476  tfsconcatb0  43789  rexanuz2nf  45935  gtnelicc  45945  xrgtnelicc  45983  limcrecl  46074  sumnnodd  46075  jumpncnp  46341  stoweidlem39  46482  stoweidlem59  46502  fourierdlem12  46562  preimagelt  47142  preimalegt  47143  pgrpgt2nabl  48857  lindslinindsimp1  48948  lmod1zrnlvec  48985  rrxsphere  49239