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

Theorem intnand 917
 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
StepHypRef Expression
1 intnand.1 . 2
2 simpr 459 . 2
31, 2nsyl 121 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 367 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 369 This theorem is referenced by:  csbxp  4905  poxp  6896  suppss2  6937  supp0cosupp0  6942  imacosupp  6943  cdadom1  8598  cfsuc  8669  axunnd  9003  difreicc  11706  fzpreddisj  11784  fzp1nel  11817  repsundef  12799  cshnz  12819  fprodntriv  13901  bitsfzo  14294  bitsmod  14295  qredeu  14457  divnumden  14490  divdenle  14491  pythagtriplem4  14552  pythagtriplem8  14556  pythagtriplem9  14557  isnsgrp  16239  isnmnd  16248  mgm2nsgrplem2  16361  0ringnnzr  18237  frlmssuvc2  19122  mamufacex  19183  mavmulsolcl  19345  maducoeval2  19434  opnfbas  20635  lgsneg  23975  usgra2edg1  24800  nbusgra  24845  cyclnspth  25048  frgra2v  25416  4cycl2vnunb  25434  2spotdisj  25478  2spotmdisj  25485  numclwwlk3lem  25525  gcdnncl  28058  divnumden2  28060  poseq  30064  nodenselem8  30148  relowlssretop  31280  relowlpssretop  31281  itg2addnclem2  31440  elpadd0  32826  dihatlat  34354  dihjatcclem1  34438  rmspecnonsq  35204  rpnnen3lem  35335  phisum  35523  gtnelicc  36902  limcrecl  37003  sumnnodd  37004  jumpncnp  37069  stoweidlem39  37189  stoweidlem59  37209  fourierdlem12  37269  usg2edgneu  38041  pgrpgt2nabl  38470  lindslinindsimp1  38569  lmod1zrnlvec  38606
 Copyright terms: Public domain W3C validator