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

Theorem intnanr 491
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 486 . 2 ((𝜑𝜓) → 𝜑)
31, 2mto 200 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 399
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 210  df-an 400
This theorem is referenced by:  falantru  1573  rab0  4320  0nelxp  5576  co02  6100  xrltnr  12511  pnfnlt  12520  nltmnf  12521  0nelfz1  12930  smu02  15834  0g0  17874  axlowdimlem13  26751  axlowdimlem16  26754  axlowdim  26758  signstfvneq0  31899  gonanegoal  32656  gonan0  32696  goaln0  32697  fmla0disjsuc  32702  bcneg1  33025  nolt02o  33256  linedegen  33661  epnsymrel  35903  padd02  37053  eldioph4b  39668  iblempty  42533  notatnand  43415  iota0ndef  43557  aiota0ndef  43578  fun2dmnopgexmpl  43766
  Copyright terms: Public domain W3C validator