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

Theorem intnanr 952
 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 187 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 196  df-an 385 This theorem is referenced by:  falantru  1499  rab0  3909  rab0OLD  3910  0nelxp  5067  co02  5566  xrltnr  11829  pnfnlt  11838  nltmnf  11839  0nelfz1  12231  smu02  15047  0g0  17086  axlowdimlem13  25634  axlowdimlem16  25637  axlowdim  25641  rusgra0edg  26482  signstfvneq0  29975  bcneg1  30875  linedegen  31420  padd02  34116  eldioph4b  36393  iblempty  38857  notatnand  39712  fun2dmnopgexmpl  40329
 Copyright terms: Public domain W3C validator