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

Theorem intnan 998
 Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
Hypothesis
Ref Expression
intnan.1 ¬ 𝜑
Assertion
Ref Expression
intnan ¬ (𝜓𝜑)

Proof of Theorem intnan
StepHypRef Expression
1 intnan.1 . 2 ¬ 𝜑
2 simpr 479 . 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:  bianfi  1004  indifdir  4027  axnulALT  4940  axnul  4941  cnv0  5694  imadif  6135  xrltnr  12167  nltmnf  12177  0nelfz1  12574  smu01  15431  3lcm2e6woprm  15551  6lcm4e12  15552  meet0  17359  join0  17360  zringndrg  20061  zclmncvs  23169  legso  25715  rgrx0ndm  26721  wwlksnext  27033  ntrl2v2e  27332  avril1  27652  helloworld  27654  topnfbey  27658  xrge00  30017  dfon2lem7  32021  nolt02o  32173  nandsym1  32749  subsym1  32754  padd01  35619  ifpdfan  38331  clsk1indlem4  38863  iblempty  40703  salexct2  41079  0nodd  42339  2nodd  42341  1neven  42461
 Copyright terms: Public domain W3C validator