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  6243  cdadom1  7828  cfsuc  7899  axunnd  8234  difreicc  10783  qredeu  12802  divnumden  12835  divdenle  12836  pythagtriplem4  12888  pythagtriplem8  12892  pythagtriplem9  12893  opnfbas  17553  lgsneg  20574  poseq  24324  nodenselem8  24413  itg2addnclem2  25004  deref  25391  hpd  26272  rmspecnonsq  27095  rpnnen3lem  27227  frlmssuvc2  27350  phisum  27621  stoweidlem39  27891  stoweidlem59  27911  nbusgra  28277  cyclnspth  28376  frgra2v  28423  4cycl2vnunb  28439  elpadd0  30620  dihatlat  32146  dihjatcclem1  32230
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