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

Theorem intnanr 999
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
Hypothesis
Ref Expression
intnan.1 ¬ 𝜑
Assertion
Ref Expression
intnanr ¬ (𝜑𝜓)

Proof of Theorem intnanr
StepHypRef Expression
1 intnan.1 . 2 ¬ 𝜑
2 simpl 474 . 2 ((𝜑𝜓) → 𝜑)
31, 2mto 188 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 383
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 197  df-an 385
This theorem is referenced by:  falantru  1657  rab0  4098  rab0OLD  4099  0nelxp  5300  co02  5810  xrltnr  12146  pnfnlt  12155  nltmnf  12156  0nelfz1  12553  smu02  15411  0g0  17464  axlowdimlem13  26033  axlowdimlem16  26036  axlowdim  26040  signstfvneq0  30958  bcneg1  31929  nolt02o  32151  linedegen  32556  epnsymrel  34631  padd02  35601  eldioph4b  37877  iblempty  40684  notatnand  41569  fun2dmnopgexmpl  41811
  Copyright terms: Public domain W3C validator