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

Theorem intnan 959
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 477 . 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:  bianfi  965  indifdir  3865  axnulALT  4757  axnul  4758  cnv0  5504  imadif  5941  xrltnr  11913  nltmnf  11923  0nelfz1  12318  smu01  15151  3lcm2e6woprm  15271  6lcm4e12  15272  meet0  17077  join0  17078  zringndrg  19778  zclmncvs  22888  legso  25428  rgrx0ndm  26393  wwlksnext  26691  ntrl2v2e  26918  avril1  27207  helloworld  27209  topnfbey  27213  xrge00  29513  dfon2lem7  31448  nandsym1  32116  subsym1  32121  padd01  34616  ifpdfan  37330  clsk1indlem4  37863  iblempty  39518  salexct2  39894  0nodd  41128  2nodd  41130  1neven  41250
  Copyright terms: Public domain W3C validator