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

Theorem intnanr 924
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 459 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2mto 180 1  |-  -.  ( ph  /\  ps )
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:  falantru  1464  rab0  3784  co02  5366  xrltnr  11423  pnfnlt  11432  nltmnf  11433  0nelfz1  11820  smu02  14454  0g0  16499  axlowdimlem13  24976  axlowdimlem16  24979  axlowdim  24983  rusgra0edg  25675  signstfvneq0  29463  bcneg1  30373  linedegen  30909  padd02  33340  eldioph4b  35617  iblempty  37706  notatnand  38240  fun2dmnopgexmpl  38770
  Copyright terms: Public domain W3C validator