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

Theorem intnan 882
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 449 . 2  |-  ( ( ps  /\  ph )  ->  ph )
31, 2mto 170 1  |-  -.  ( ps  /\  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 360
This theorem is referenced by:  bianfi  893  indifdir  3599  axnulALT  4339  axnul  4340  imadif  5531  xrltnr  10725  nltmnf  10731  smu01  13003  avril1  21762  helloworld  21764  xrge00  24213  dfon2lem7  25421  nandsym1  26177  subsym1  26182  padd01  30682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator