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

Theorem intnanr 981
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 472 . 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  1548  rab0  3988  rab0OLD  3989  0nelxp  5177  co02  5687  xrltnr  11991  pnfnlt  12000  nltmnf  12001  0nelfz1  12398  smu02  15256  0g0  17310  axlowdimlem13  25879  axlowdimlem16  25882  axlowdim  25886  signstfvneq0  30777  bcneg1  31748  nolt02o  31970  linedegen  32375  padd02  35416  eldioph4b  37692  iblempty  40499  notatnand  41384  fun2dmnopgexmpl  41626
  Copyright terms: Public domain W3C validator