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

Theorem intnan 488
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 486 . 2 ((𝜓𝜑) → 𝜑)
31, 2mto 196 1 ¬ (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 397
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 206  df-an 398
This theorem is referenced by:  bianfi  535  indifdirOLD  4246  noel  4291  noelOLD  4292  axnulALT  5262  axnul  5263  cnv0  6094  imadif  6586  poxp3  8083  xrltnr  13045  nltmnf  13055  0nelfz1  13466  smu01  16371  3lcm2e6woprm  16496  6lcm4e12  16497  join0  18299  meet0  18300  nsmndex1  18728  smndex2dnrinv  18730  zringndrg  20905  zclmncvs  24528  nolt02o  27059  nogt01o  27060  legso  27583  rgrx0ndm  28583  wwlksnext  28880  ntrl2v2e  29144  avril1  29449  helloworld  29451  topnfbey  29455  xrge00  31926  fmlaomn0  34041  gonan0  34043  goaln0  34044  prv0  34081  dfon2lem7  34420  nandsym1  34940  bj-inftyexpitaudisj  35722  padd01  38320  ifpdfan  41826  sucomisnotcard  41904  clsk1indlem4  42404  iblempty  44292  salexct2  44666  0nodd  46190  2nodd  46192  1neven  46316  ipolub00  47104
  Copyright terms: Public domain W3C validator