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

Theorem intnan 951
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 476 . 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:  bianfi  962  indifdir  3842  axnulALT  4710  axnul  4711  imadif  5873  xrltnr  11793  nltmnf  11803  0nelfz1  12189  smu01  14995  3lcm2e6woprm  15115  6lcm4e12  15116  meet0  16909  join0  16910  legso  25240  wwlknext  26046  avril1  26505  helloworld  26507  topnfbey  26511  xrge00  28811  dfon2lem7  30732  nandsym1  31385  subsym1  31390  padd01  33909  ifpdfan  36623  clsk1indlem4  37156  iblempty  38651  salexct2  39027  rgrx0ndm  40785  wwlksnext  41091  ntrl2v2e  41317  0nodd  41592  2nodd  41594  1neven  41714
  Copyright terms: Public domain W3C validator