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

Theorem intnanrd 918
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 455 . 2  |-  ( ( ps  /\  ch )  ->  ps )
31, 2nsyl 121 1  |-  ( ph  ->  -.  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  bianfd  927  3bior1fand  1337  wemappo  8008  axrepnd  9001  axunnd  9003  fzpreddisj  11784  sadadd2lem2  14309  smumullem  14351  sqgcd  14405  coprm  14450  divgcdodd  14469  pythagtriplem19  14566  isnmnd  16248  nfimdetndef  19383  mdetfval1  19384  ibladdlem  22518  lgsval2lem  23962  lgsval4a  23974  lgsdilem  23978  uvtx01vtx  24909  clwlknclwlkdifs  25377  frgra2v  25416  2sqcoprm  28087  nodenselem8  30148  dfrdg4  30289  ibladdnclem  31444  dihatlat  34354  jm2.23  35300  lcmgcdlem  36060  ltnelicc  36899  limciccioolb  36995  dvmptfprodlem  37109  stoweidlem26  37176  fourierdlem12  37269  fourierdlem42  37299  divgcdoddALTV  37764  pr1eqbg  37930
  Copyright terms: Public domain W3C validator