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

Theorem intnan 923
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 463 . 2  |-  ( ( ps  /\  ph )  ->  ph )
31, 2mto 180 1  |-  -.  ( ps  /\  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  bianfi  934  indifdir  3730  axnulALT  4550  axnul  4551  axnulOLD  4552  imadif  5674  xrltnr  11423  nltmnf  11433  0nelfz1  11820  smu01  14453  3lcm2e6woprm  14573  6lcm4e12  14574  meet0  16376  join0  16377  legso  24636  wwlknext  25444  avril1  25892  helloworld  25894  topnfbey  25898  xrge00  28449  dfon2lem7  30436  nandsym1  31081  subsym1  31086  padd01  33301  ifpdfan  36035  iblempty  37668  0nodd  39114  2nodd  39116  1neven  39236
  Copyright terms: Public domain W3C validator