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

Theorem intnanr 487
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 482 . 2 ((𝜑𝜓) → 𝜑)
31, 2mto 197 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395
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 207  df-an 396
This theorem is referenced by:  falantru  1575  rab0  4386  0nelopab  5572  0nelxp  5719  co02  6280  xrltnr  13161  pnfnlt  13170  nltmnf  13171  0nelfz1  13583  smu02  16524  0g0  18677  nolt02o  27740  nogt01o  27741  axlowdimlem13  28969  axlowdimlem16  28972  axlowdim  28976  signstfvneq0  34587  gonanegoal  35357  gonan0  35397  goaln0  35398  fmla0disjsuc  35403  bcneg1  35736  linedegen  36144  epnsymrel  38563  padd02  39814  eldioph4b  42822  iblempty  45980  notatnand  46908  iota0ndef  47051  aiota0ndef  47109  fun2dmnopgexmpl  47296
  Copyright terms: Public domain W3C validator