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

Theorem intnan 912
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 459 . 2  |-  ( ( ps  /\  ph )  ->  ph )
31, 2mto 176 1  |-  -.  ( ps  /\  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  bianfi  923  indifdir  3751  axnulALT  4566  axnul  4567  imadif  5645  xrltnr  11333  nltmnf  11341  smu01  14220  meet0  15966  join0  15967  legso  24186  wwlknext  24926  avril1  25373  helloworld  25375  xrge00  27908  dfon2lem7  29461  nandsym1  30115  subsym1  30120  iblempty  32003  0nodd  32870  2nodd  32872  1neven  32992  padd01  35932  ifpdfan  38134
  Copyright terms: Public domain W3C validator