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

Theorem intnanr 906
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 457 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2mto 176 1  |-  -.  ( ph  /\  ps )
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:  falantru  1396  rab0  3769  co02  5462  xrltnr  11215  pnfnlt  11222  nltmnf  11223  smu02  13804  0g0  15556  axlowdimlem13  23372  axlowdimlem16  23375  axlowdim  23379  signstfvneq0  27137  linedegen  28338  eldioph4b  29318  notatnand  30078  rusgra0edg  30741  padd02  33814
  Copyright terms: Public domain W3C validator