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

Theorem intnanr 476
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 469 . 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 198  df-an 384
This theorem is referenced by:  falantru  1659  rab0  4113  0nelxp  5296  co02  5804  xrltnr  12175  pnfnlt  12184  nltmnf  12185  0nelfz1  12589  smu02  15438  0g0  17491  axlowdimlem13  26076  axlowdimlem16  26079  axlowdim  26083  signstfvneq0  31006  bcneg1  31977  nolt02o  32199  linedegen  32604  epnsymrel  34665  padd02  35636  eldioph4b  37916  iblempty  40704  notatnand  41589  iota0ndef  41698  aiota0ndef  41712  fun2dmnopgexmpl  41850
  Copyright terms: Public domain W3C validator