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

Theorem intnand 914
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  5079  poxp  6892  suppss2  6931  supp0cosupp0  6936  imacosupp  6937  cdadom1  8562  cfsuc  8633  axunnd  8967  difreicc  11648  fzpreddisj  11725  swrd0  12617  repsundef  12702  cshnz  12722  bitsfzo  13940  bitsmod  13941  qredeu  14103  divnumden  14136  divdenle  14137  pythagtriplem4  14198  pythagtriplem8  14202  pythagtriplem9  14203  frlmssuvc2  18593  frlmssuvc2OLD  18595  mamufacex  18658  mavmulsolcl  18820  maducoeval2  18909  opnfbas  20078  lgsneg  23322  usgra2edg1  24059  nbusgra  24104  cyclnspth  24307  frgra2v  24675  4cycl2vnunb  24693  2spotdisj  24738  2spotmdisj  24745  numclwwlk3lem  24785  divnumden2  27276  fzp1nel  28593  fprodntriv  28651  poseq  28910  nodenselem8  29025  itg2addnclem2  29644  rmspecnonsq  30447  rpnnen3lem  30577  phisum  30764  gtnelicc  31097  limcrecl  31171  jumpncnp  31237  stoweidlem39  31339  stoweidlem59  31359  fourierdlem12  31419  usg2edgneu  31881  pgrpgt2nabl  32024  0rngnnzr  32031  lindslinindsimp1  32131  lmod1zrnlvec  32176  elpadd0  34605  dihatlat  36131  dihjatcclem1  36215
  Copyright terms: Public domain W3C validator