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

Theorem intnanrd 908
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  917  3bior1fand  1325  wemappo  7782  axrepnd  8777  axunnd  8779  fzpreddisj  11523  swrd0  12346  sadadd2lem2  13665  smumullem  13707  sqgcd  13761  coprm  13805  divgcdodd  13824  pythagtriplem19  13919  nfimdetndef  18419  mdetfval1  18420  ibladdlem  21316  lgsval2lem  22664  lgsval4a  22676  lgsdilem  22680  uvtx01vtx  23419  nodenselem8  27848  dfrdg4  28000  ibladdnclem  28471  jm2.23  29368  stoweidlem26  29844  pr1eqbg  30144  clwlknclwlkdifs  30601  frgra2v  30614  dihatlat  35002
  Copyright terms: Public domain W3C validator