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

Theorem intnanr 960
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 473 . 2 ((𝜑𝜓) → 𝜑)
31, 2mto 188 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 384
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 386
This theorem is referenced by:  falantru  1505  rab0  3934  rab0OLD  3935  0nelxp  5108  co02  5611  xrltnr  11897  pnfnlt  11906  nltmnf  11907  0nelfz1  12299  smu02  15128  0g0  17179  axlowdimlem13  25729  axlowdimlem16  25732  axlowdim  25736  signstfvneq0  30421  bcneg1  31322  linedegen  31884  padd02  34564  eldioph4b  36841  iblempty  39475  notatnand  40354  fun2dmnopgexmpl  40588
  Copyright terms: Public domain W3C validator