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

Theorem intnand 883
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 448 . 2  |-  ( ( ch  /\  ps )  ->  ps )
31, 2nsyl 115 1  |-  ( ph  ->  -.  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359
This theorem is referenced by:  poxp  6450  cdadom1  8058  cfsuc  8129  axunnd  8463  difreicc  11020  bitsfzo  12939  bitsmod  12940  qredeu  13099  divnumden  13132  divdenle  13133  pythagtriplem4  13185  pythagtriplem8  13189  pythagtriplem9  13190  opnfbas  17866  lgsneg  21095  usgra2edg1  21395  nbusgra  21432  cyclnspth  21610  divnumden2  24153  fzp1nel  25202  fprodntriv  25260  poseq  25520  nodenselem8  25635  itg2addnclem2  26247  rmspecnonsq  26961  rpnnen3lem  27093  frlmssuvc2  27215  phisum  27486  stoweidlem39  27755  stoweidlem59  27775  cshnnn0  28202  frgra2v  28326  4cycl2vnunb  28344  2spotdisj  28387  2spotmdisj  28394  elpadd0  30543  dihatlat  32069  dihjatcclem1  32153
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 178  df-an 361
  Copyright terms: Public domain W3C validator