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

Theorem intnan 880
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
Hypothesis
Ref Expression
intnan.1  |-  -.  ph
Assertion
Ref Expression
intnan  |-  -.  ( ps  /\  ph )

Proof of Theorem intnan
StepHypRef Expression
1 intnan.1 . 2  |-  -.  ph
2 simpr 447 . 2  |-  ( ( ps  /\  ph )  ->  ph )
31, 2mto 167 1  |-  -.  ( ps  /\  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 358
This theorem is referenced by:  bianfi  891  truanfal  1327  indifdir  3425  axnulALT  4147  axnul  4148  imadif  5327  xrltnr  10462  nltmnf  10468  smu01  12677  avril1  20836  helloworld  20838  dfon2lem7  24145  nandsym1  24861  subsym1  24866  padd01  30000
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