Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  intnanrd Unicode version

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
StepHypRef Expression
1 intnand.1 . 2
2 simpl 457 . 2
31, 2nsyl 121 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator