Theorem intnanrd 917

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1

Assertion

Ref	Expression
intnanrd

Proof of Theorem intnanrd

Step	Hyp	Ref	Expression
1		intnand.1	. 2
2		simpl 457	. 2
3	1, 2	nsyl 121	1

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

This theorem is referenced by:  bianfd  926  3bior1fand  1335  wemappo  7995  axrepnd  8990  axunnd  8992  fzpreddisj  11758  swrd0  12658  sadadd2lem2  14100  smumullem  14142  sqgcd  14196  coprm  14241  divgcdodd  14260  pythagtriplem19  14357  isnmnd  15924  nfimdetndef  19091  mdetfval1  19092  ibladdlem  22226  lgsval2lem  23581  lgsval4a  23593  lgsdilem  23597  uvtx01vtx  24492  clwlknclwlkdifs  24960  frgra2v  24999  2sqcoprm  27635  nodenselem8  29448  dfrdg4  29600  ibladdnclem  30071  jm2.23  30938  lcmgcdlem  31212  ltnelicc  31530  limciccioolb  31627  dvmptfprodlem  31741  stoweidlem26  31808  fourierdlem12  31901  fourierdlem42  31931  pr1eqbg  32297  dihatlat  37061

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