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

Theorem intnand 882
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 447 . 2  |-  ( ( ch  /\  ps )  ->  ps )
31, 2nsyl 113 1  |-  ( ph  ->  -.  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  poxp  6227  cdadom1  7812  cfsuc  7883  axunnd  8218  difreicc  10767  qredeu  12786  divnumden  12819  divdenle  12820  pythagtriplem4  12872  pythagtriplem8  12876  pythagtriplem9  12877  opnfbas  17537  lgsneg  20558  poseq  24253  nodenselem8  24342  deref  25288  hpd  26169  rmspecnonsq  26992  rpnnen3lem  27124  frlmssuvc2  27247  phisum  27518  stoweidlem39  27788  stoweidlem59  27808  nbusgra  28143  frgra2v  28177  elpadd0  29998  dihatlat  31524  dihjatcclem1  31608
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator