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  3438  axnulALT  4163  axnul  4164  imadif  5343  xrltnr  10478  nltmnf  10484  smu01  12693  avril1  20852  helloworld  20854  dfon2lem7  24216  nandsym1  24933  subsym1  24938  padd01  30622
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