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

Theorem intnanr 931
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
Hypothesis
Ref Expression
intnan.1  |-  -.  ph
Assertion
Ref Expression
intnanr  |-  -.  ( ph  /\  ps )

Proof of Theorem intnanr
StepHypRef Expression
1 intnan.1 . 2  |-  -.  ph
2 simpl 463 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2mto 181 1  |-  -.  ( ph  /\  ps )
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:  falantru  1478  rab0  3764  co02  5367  xrltnr  11449  pnfnlt  11458  nltmnf  11459  0nelfz1  11846  smu02  14509  0g0  16554  axlowdimlem13  25032  axlowdimlem16  25035  axlowdim  25039  rusgra0edg  25731  signstfvneq0  29509  bcneg1  30420  linedegen  30958  padd02  33421  eldioph4b  35698  iblempty  37879  notatnand  38520  fun2dmnopgexmpl  39069
  Copyright terms: Public domain W3C validator