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

Theorem intnan 490
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 488 . 2 ((𝜓𝜑) → 𝜑)
31, 2mto 200 1 ¬ (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 399
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 210  df-an 400
This theorem is referenced by:  bianfi  537  indifdirOLD  4174  noel  4217  noelOLD  4218  dfopif  4752  axnulALT  5169  axnul  5170  cnv0  5967  imadif  6417  xrltnr  12590  nltmnf  12600  0nelfz1  13010  smu01  15922  3lcm2e6woprm  16049  6lcm4e12  16050  meet0  17856  join0  17857  nsmndex1  18187  smndex2dnrinv  18189  zringndrg  20302  zclmncvs  23893  legso  26537  rgrx0ndm  27527  wwlksnext  27823  ntrl2v2e  28087  avril1  28392  helloworld  28394  topnfbey  28398  xrge00  30864  fmlaomn0  32915  gonan0  32917  goaln0  32918  prv0  32955  dfon2lem7  33329  poxp3  33399  nolt02o  33531  nogt01o  33532  nandsym1  34241  subsym1  34246  bj-inftyexpitaudisj  34986  padd01  37437  ifpdfan  40611  clsk1indlem4  41184  iblempty  43032  salexct2  43404  0nodd  44882  2nodd  44884  1neven  45008
  Copyright terms: Public domain W3C validator