MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  intnand 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  6394  cdadom1  7999  cfsuc  8070  axunnd  8404  difreicc  10960  bitsfzo  12874  bitsmod  12875  qredeu  13034  divnumden  13067  divdenle  13068  pythagtriplem4  13120  pythagtriplem8  13124  pythagtriplem9  13125  opnfbas  17795  lgsneg  20970  usgra2edg1  21269  nbusgra  21306  cyclnspth  21466  divnumden2  23999  fzp1nel  24989  fprodntriv  25047  poseq  25277  nodenselem8  25366  itg2addnclem2  25958  rmspecnonsq  26661  rpnnen3lem  26793  frlmssuvc2  26916  phisum  27187  stoweidlem39  27456  stoweidlem59  27476  frgra2v  27752  4cycl2vnunb  27770  elpadd0  29923  dihatlat  31449  dihjatcclem1  31533
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