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

Theorem intnan 930
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 467 . 2  |-  ( ( ps  /\  ph )  ->  ph )
31, 2mto 181 1  |-  -.  ( ps  /\  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  bianfi  941  indifdir  3710  axnulALT  4544  axnul  4545  axnulOLD  4546  imadif  5679  xrltnr  11449  nltmnf  11459  0nelfz1  11846  smu01  14508  3lcm2e6woprm  14628  6lcm4e12  14629  meet0  16431  join0  16432  legso  24692  wwlknext  25500  avril1  25948  helloworld  25950  topnfbey  25954  xrge00  28496  dfon2lem7  30483  nandsym1  31130  subsym1  31135  padd01  33420  ifpdfan  36153  iblempty  37879  salexct2  38235  rgrx0ndm  39657  ntrl2v2e  39872  0nodd  40082  2nodd  40084  1neven  40204
  Copyright terms: Public domain W3C validator