Theorem intnand 916

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 461	. 2
3	1, 2	nsyl 121	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369

This theorem is referenced by:  csbxp  5086  poxp  6912  suppss2  6953  supp0cosupp0  6958  imacosupp  6959  cdadom1  8587  cfsuc  8658  axunnd  8992  difreicc  11681  fzpreddisj  11758  fzp1nel  11791  swrd0  12658  repsundef  12743  cshnz  12763  fprodntriv  13749  bitsfzo  14085  bitsmod  14086  qredeu  14248  divnumden  14281  divdenle  14282  pythagtriplem4  14343  pythagtriplem8  14347  pythagtriplem9  14348  isnsgrp  15915  isnmnd  15924  mgm2nsgrplem2  16037  0ringnnzr  17917  frlmssuvc2  18826  frlmssuvc2OLD  18828  mamufacex  18891  mavmulsolcl  19053  maducoeval2  19142  opnfbas  20343  lgsneg  23594  usgra2edg1  24383  nbusgra  24428  cyclnspth  24631  frgra2v  24999  4cycl2vnunb  25017  2spotdisj  25061  2spotmdisj  25068  numclwwlk3lem  25108  gcdnncl  27607  divnumden2  27609  poseq  29333  nodenselem8  29448  itg2addnclem2  30067  rmspecnonsq  30843  rpnnen3lem  30973  phisum  31159  gtnelicc  31533  limcrecl  31635  sumnnodd  31636  jumpncnp  31701  stoweidlem39  31821  stoweidlem59  31841  fourierdlem12  31901  usg2edgneu  32412  pgrpgt2nabl  32959  lindslinindsimp1  33058  lmod1zrnlvec  33095  elpadd0  35533  dihatlat  37061  dihjatcclem1  37145

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 185  df-an 371