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

Theorem intnanr 914
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 455 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2mto 176 1  |-  -.  ( ph  /\  ps )
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:  falantru  1429  rab0  3757  co02  5456  xrltnr  11299  pnfnlt  11306  nltmnf  11307  smu02  14236  0g0  16104  axlowdimlem13  24556  axlowdimlem16  24559  axlowdim  24563  rusgra0edg  25254  signstfvneq0  28916  bcneg1  29826  linedegen  30449  padd02  32793  eldioph4b  35070  iblempty  37099  notatnand  37426
  Copyright terms: Public domain W3C validator