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  1328  rab0  3475  co02  5186  xrltnr  10462  pnfnlt  10467  nltmnf  10468  0g0  14386  axlowdimlem13  24582  axlowdimlem16  24585  axlowdim  24589  linedegen  24766  eldioph4b  26894  padd02  30001
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