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  7264  axrepnd  8216  axunnd  8218  smumullem  12683  sqgcd  12737  coprm  12779  divgcdodd  12798  pythagtriplem19  12886  ibladdlem  19174  lgsval2lem  20545  lgsval4a  20557  lgsdilem  20561  nodenselem8  24342  dfrdg4  24488  jm2.23  27089  stoweidlem26  27775  uvtx01vtx  28164  frgra2v  28177  dihatlat  31524
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