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

Theorem intnanrd 915
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 457 . 2  |-  ( ( ps  /\  ch )  ->  ps )
31, 2nsyl 121 1  |-  ( ph  ->  -.  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  bianfd  924  3bior1fand  1335  wemappo  7974  axrepnd  8969  axunnd  8971  fzpreddisj  11729  swrd0  12621  sadadd2lem2  13959  smumullem  14001  sqgcd  14055  coprm  14100  divgcdodd  14119  pythagtriplem19  14216  nfimdetndef  18886  mdetfval1  18887  ibladdlem  21989  lgsval2lem  23337  lgsval4a  23349  lgsdilem  23353  uvtx01vtx  24196  clwlknclwlkdifs  24664  frgra2v  24703  nodenselem8  29053  dfrdg4  29205  ibladdnclem  29676  jm2.23  30570  lcmgcdlem  30840  ltnelicc  31122  limciccioolb  31191  stoweidlem26  31354  fourierdlem12  31447  fourierdlem42  31477  pr1eqbg  31792  dihatlat  36149
  Copyright terms: Public domain W3C validator