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

Theorem intnan 480
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 198  df-an 385
This theorem is referenced by:  bianfi  529  indifdir  4048  axnulALT  4947  axnul  4948  cnv0  5718  imadif  6151  xrltnr  12153  nltmnf  12163  0nelfz1  12567  smu01  15491  3lcm2e6woprm  15611  6lcm4e12  15612  meet0  17405  join0  17406  zringndrg  20111  zclmncvs  23226  legso  25785  rgrx0ndm  26780  wwlksnext  27093  ntrl2v2e  27394  avril1  27713  helloworld  27715  topnfbey  27719  xrge00  30068  dfon2lem7  32069  nolt02o  32221  nandsym1  32792  subsym1  32797  padd01  35699  ifpdfan  38418  clsk1indlem4  38948  iblempty  40750  salexct2  41126  0nodd  42411  2nodd  42413  1neven  42533
  Copyright terms: Public domain W3C validator