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

Theorem intnanrd 933
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 463 . 2  |-  ( ( ps  /\  ch )  ->  ps )
31, 2nsyl 126 1  |-  ( ph  ->  -.  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190  df-an 377
This theorem is referenced by:  bianfd  942  3bior1fand  1386  wemappo  8095  axrepnd  9050  axunnd  9052  fzpreddisj  11880  sadadd2lem2  14479  smumullem  14521  nndvdslegcd  14534  sqgcd  14581  divgcdodd  14708  coprm  14712  pythagtriplem19  14838  isnmnd  16595  nfimdetndef  19669  mdetfval1  19670  ibladdlem  22833  lgsval2lem  24290  lgsval4a  24302  lgsdilem  24306  uvtx01vtx  25276  clwlknclwlkdifs  25744  frgra2v  25783  2sqcoprm  28460  nodenselem8  30627  dfrdg4  30768  finxpreclem3  31831  finxpreclem5  31833  ibladdnclem  32044  dihatlat  34948  jm2.23  35897  ltnelicc  37679  limciccioolb  37787  dvmptfprodlem  37905  stoweidlem26  37987  fourierdlem12  38082  fourierdlem42  38113  fourierdlem42OLD  38114  divgcdoddALTV  38946  pr1eqbg  39128  nbgrnself  39575
  Copyright terms: Public domain W3C validator