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

Theorem intnanr 881
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
Hypothesis
Ref Expression
intnan.1  |-  -.  ph
Assertion
Ref Expression
intnanr  |-  -.  ( ph  /\  ps )

Proof of Theorem intnanr
StepHypRef Expression
1 intnan.1 . 2  |-  -.  ph
2 simpl 443 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2mto 167 1  |-  -.  ( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 358
This theorem is referenced by:  falantru  1329  rab0  3509  co02  5223  xrltnr  10509  pnfnlt  10514  nltmnf  10515  0g0  14435  axlowdimlem13  24968  axlowdimlem16  24971  axlowdim  24975  linedegen  25152  eldioph4b  26042  wlkntrllem2  27462  padd02  29819
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 177  df-an 360
  Copyright terms: Public domain W3C validator