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

Theorem intnan 487
 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 485 . 2 ((𝜓𝜑) → 𝜑)
31, 2mto 198 1 ¬ (𝜓𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 396 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 208  df-an 397 This theorem is referenced by:  bianfi  534  indifdir  4264  noel  4300  axnulALT  5205  axnul  5206  cnv0  5998  imadif  6437  xrltnr  12509  nltmnf  12519  0nelfz1  12921  smu01  15830  3lcm2e6woprm  15954  6lcm4e12  15955  meet0  17742  join0  17743  zringndrg  20572  zclmncvs  23686  legso  26318  rgrx0ndm  27308  wwlksnext  27604  ntrl2v2e  27870  avril1  28175  helloworld  28177  topnfbey  28181  xrge00  30606  fmlaomn0  32540  gonan0  32542  goaln0  32543  prv0  32580  dfon2lem7  32937  nolt02o  33102  nandsym1  33673  subsym1  33678  bj-inftyexpitaudisj  34385  padd01  36833  ifpdfan  39715  clsk1indlem4  40278  iblempty  42134  salexct2  42507  0nodd  43928  2nodd  43930  nsmndex1  43987  smndex2dnrinv  43989  1neven  44105
 Copyright terms: Public domain W3C validator