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  5726  poxp  8072  frxp3  8095  poseq  8102  suppss2  8144  suppco  8150  cfsuc  10173  axunnd  10513  difreicc  13431  fzpreddisj  13521  fzp1nel  13559  repsundef  14727  cshnz  14748  fprodntriv  15901  bitsfzo  16398  bitsmod  16399  gcdnncl  16470  gcd2n0cl  16472  qredeu  16621  cncongr2  16631  divnumden  16712  divdenle  16713  phisum  16755  pythagtriplem4  16784  pythagtriplem8  16788  pythagtriplem9  16789  cat1lem  18057  isnsgrp  18685  isnmnd  18700  mgm2nsgrplem2  18884  0ringnnzr  20496  frlmssuvc2  21788  psdmul  22145  mamufacex  22374  mavmulsolcl  22529  maducoeval2  22618  opnfbas  23820  lgsneg  27301  nodenselem8  27672  noinfbnd2lem1  27711  pw2cut2  28471  numedglnl  29230  umgredgnlp  29233  umgr2edg1  29297  umgr2edgneu  29300  uhgrnbgr0nb  29440  nfrgr2v  30360  4cycl2vnunb  30378  hashxpe  32898  elq2  32903  divnumden2  32907  esplyfval3  33734  fmlasucdisj  35600  weiunpo  36666  weiunfr  36668  unbdqndv1  36787  relowlssretop  37696  relowlpssretop  37697  finxpreclem6  37729  itg2addnclem2  38010  elpadd0  40272  dihatlat  41797  dihjatcclem1  41881  aks4d1p8d1  42540  sticksstones22  42624  rmspecnonsq  43356  rpnnen3lem  43480  tfsconcatb0  43793  rexanuz2nf  45941  gtnelicc  45951  xrgtnelicc  45989  limcrecl  46080  sumnnodd  46081  jumpncnp  46347  stoweidlem39  46488  stoweidlem59  46508  fourierdlem12  46568  preimagelt  47148  preimalegt  47149  pgrpgt2nabl  48857  lindslinindsimp1  48948  lmod1zrnlvec  48985  rrxsphere  49239