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

Theorem intnand 907
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
Hypothesis
Ref Expression
intnand.1  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
intnand  |-  ( ph  ->  -.  ( ch  /\  ps ) )

Proof of Theorem intnand
StepHypRef Expression
1 intnand.1 . 2  |-  ( ph  ->  -.  ps )
2 simpr 461 . 2  |-  ( ( ch  /\  ps )  ->  ps )
31, 2nsyl 121 1  |-  ( ph  ->  -.  ( ch  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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
This theorem is referenced by:  csbxp  4933  poxp  6699  suppss2  6738  supp0cosupp0  6743  imacosupp  6744  cdadom1  8370  cfsuc  8441  axunnd  8775  difreicc  11432  fzpreddisj  11519  swrd0  12342  repsundef  12424  cshnz  12444  bitsfzo  13646  bitsmod  13647  qredeu  13808  divnumden  13841  divdenle  13842  pythagtriplem4  13901  pythagtriplem8  13905  pythagtriplem9  13906  frlmssuvc2  18235  frlmssuvc2OLD  18237  mamufacex  18304  mavmulsolcl  18377  maducoeval2  18461  opnfbas  19430  lgsneg  22673  usgra2edg1  23317  nbusgra  23354  cyclnspth  23532  divnumden2  26102  fzp1nel  27412  fprodntriv  27470  poseq  27729  nodenselem8  27844  itg2addnclem2  28463  rmspecnonsq  29267  rpnnen3lem  29399  phisum  29586  stoweidlem39  29853  stoweidlem59  29873  frgra2v  30610  4cycl2vnunb  30628  2spotdisj  30673  2spotmdisj  30680  numclwwlk3lem  30720  pgrpgt2nabel  30788  0rngnnzr  30797  lindslinindsimp1  31010  lmod1zrnlvec  31055  elpadd0  33472  dihatlat  34998  dihjatcclem1  35082
  Copyright terms: Public domain W3C validator