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

Theorem intnanr 483
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 476 . 2 ((𝜑𝜓) → 𝜑)
31, 2mto 189 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 386
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 199  df-an 387
This theorem is referenced by:  falantru  1692  rab0  4187  0nelxp  5380  co02  5894  xrltnr  12246  pnfnlt  12255  nltmnf  12256  0nelfz1  12660  smu02  15589  0g0  17623  axlowdimlem13  26260  axlowdimlem16  26263  axlowdim  26267  signstfvneq0  31193  bcneg1  32160  nolt02o  32379  linedegen  32784  epnsymrel  34851  padd02  35882  eldioph4b  38214  iblempty  40969  notatnand  41851  iota0ndef  41964  aiota0ndef  41986  fun2dmnopgexmpl  42181
  Copyright terms: Public domain W3C validator