MPE Home 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  4026  axnulALT  4939  axnul  4940  cnv0  5693  imadif  6134  xrltnr  12146  nltmnf  12156  0nelfz1  12553  smu01  15410  3lcm2e6woprm  15530  6lcm4e12  15531  meet0  17338  join0  17339  zringndrg  20040  zclmncvs  23148  legso  25693  rgrx0ndm  26699  wwlksnext  27011  ntrl2v2e  27310  avril1  27630  helloworld  27632  topnfbey  27636  xrge00  29995  dfon2lem7  31999  nolt02o  32151  nandsym1  32727  subsym1  32732  padd01  35600  ifpdfan  38312  clsk1indlem4  38844  iblempty  40684  salexct2  41060  0nodd  42320  2nodd  42322  1neven  42442
  Copyright terms: Public domain W3C validator