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

Theorem intnanr 486
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 481 . 2 ((𝜑𝜓) → 𝜑)
31, 2mto 196 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 394
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 206  df-an 395
This theorem is referenced by:  falantru  1568  rab0  4384  0nelopab  5571  0nelxp  5714  co02  6267  xrltnr  13137  pnfnlt  13146  nltmnf  13147  0nelfz1  13558  smu02  16467  0g0  18629  nolt02o  27646  nogt01o  27647  axlowdimlem13  28783  axlowdimlem16  28786  axlowdim  28790  signstfvneq0  34209  gonanegoal  34967  gonan0  35007  goaln0  35008  fmla0disjsuc  35013  bcneg1  35335  linedegen  35744  epnsymrel  38038  padd02  39289  eldioph4b  42234  iblempty  45355  notatnand  46280  iota0ndef  46423  aiota0ndef  46479  fun2dmnopgexmpl  46666
  Copyright terms: Public domain W3C validator