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  4715  axnul  4716  cnv0  5454  imadif  5887  xrltnr  11829  nltmnf  11839  0nelfz1  12231  smu01  15046  3lcm2e6woprm  15166  6lcm4e12  15167  meet0  16960  join0  16961  zringndrg  19657  zclmncvs  22756  legso  25294  wwlknext  26252  avril1  26711  helloworld  26713  topnfbey  26717  xrge00  29017  dfon2lem7  30938  nandsym1  31591  subsym1  31596  padd01  34115  ifpdfan  36829  clsk1indlem4  37362  iblempty  38857  salexct2  39233  rgrx0ndm  40793  wwlksnext  41099  ntrl2v2e  41325  0nodd  41600  2nodd  41602  1neven  41722
 Copyright terms: Public domain W3C validator