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

Theorem intnan 881
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 448 . 2  |-  ( ( ps  /\  ph )  ->  ph )
31, 2mto 169 1  |-  -.  ( ps  /\  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 359
This theorem is referenced by:  bianfi  892  indifdir  3565  axnulALT  4304  axnul  4305  imadif  5495  xrltnr  10684  nltmnf  10690  smu01  12961  avril1  21718  helloworld  21720  xrge00  24169  dfon2lem7  25367  nandsym1  26084  subsym1  26089  padd01  30305
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 178  df-an 361
  Copyright terms: Public domain W3C validator