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

Theorem intnan 905
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 461 . 2  |-  ( ( ps  /\  ph )  ->  ph )
31, 2mto 176 1  |-  -.  ( ps  /\  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 369
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 371
This theorem is referenced by:  bianfi  916  indifdir  3706  axnulALT  4519  axnul  4520  imadif  5593  xrltnr  11204  nltmnf  11212  smu01  13786  meet0  15411  join0  15412  avril1  23793  helloworld  23795  xrge00  26283  dfon2lem7  27738  nandsym1  28404  subsym1  28409  wwlknext  30496  padd01  33763
  Copyright terms: Public domain W3C validator