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

Theorem intnanr 882
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 444 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2mto 169 1  |-  -.  ( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 359
This theorem is referenced by:  falantru  1347  rab0  3648  co02  5383  xrltnr  10720  pnfnlt  10725  nltmnf  10726  smu02  12999  0g0  14709  axlowdimlem13  25893  axlowdimlem16  25896  axlowdim  25900  linedegen  26077  eldioph4b  26872  notatnand  27840  padd02  30609
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator