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

Theorem intnanrd 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
intnanrd  |-  ( ph  ->  -.  ( ps  /\  ch ) )

Proof of Theorem intnanrd
StepHypRef Expression
1 intnand.1 . 2  |-  ( ph  ->  -.  ps )
2 simpl 443 . 2  |-  ( ( ps  /\  ch )  ->  ps )
31, 2nsyl 113 1  |-  ( ph  ->  -.  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  bianfd  892  wemappo  7280  axrepnd  8232  axunnd  8234  smumullem  12699  sqgcd  12753  coprm  12795  divgcdodd  12814  pythagtriplem19  12902  ibladdlem  19190  lgsval2lem  20561  lgsval4a  20573  lgsdilem  20577  nodenselem8  24413  dfrdg4  24560  ibladdnclem  25007  jm2.23  27192  stoweidlem26  27878  3bior1fand  28178  uvtx01vtx  28305  frgra2v  28423  dihatlat  32146
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