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

Theorem intnanrd 885
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 445 . 2  |-  ( ( ps  /\  ch )  ->  ps )
31, 2nsyl 116 1  |-  ( ph  ->  -.  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 360
This theorem is referenced by:  bianfd  894  3bior1fand  1291  wemappo  7519  axrepnd  8470  axunnd  8472  sadadd2lem2  12963  smumullem  13005  sqgcd  13059  coprm  13101  divgcdodd  13120  pythagtriplem19  13208  ibladdlem  19712  lgsval2lem  21091  lgsval4a  21103  lgsdilem  21107  uvtx01vtx  21502  nodenselem8  25644  dfrdg4  25796  ibladdnclem  26262  jm2.23  27068  stoweidlem26  27752  pr1eqbg  28057  frgra2v  28390  dihatlat  32133
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 179  df-an 362
  Copyright terms: Public domain W3C validator