Theorem intnan 491

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

Step	Hyp	Ref	Expression
1		intnan.1	. 2 ⊢ ¬ 𝜑
2		simpr 489	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 200	1 ⊢ ¬ (𝜓 ∧ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 400

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 401

This theorem is referenced by:  bianfi  542  noel  4299  uni0  4902  axnulALT  5266  axnul  5267  cnv0  5867  cnv0OLD  5868  imadif  6618  poxp3  8142  1div0  11869  xrltnr  13140  nltmnf  13150  0nelfz1  13567  smu01  16540  3lcm2e6woprm  16669  6lcm4e12  16670  join0  18455  meet0  18456  nsmndex1  18971  smndex2dnrinv  18973  zringndrg  21583  zclmncvs  25272  nolt02o  27821  nogt01o  27822  legso  28830  rgrx0ndm  29880  wwlksnext  30179  ntrl2v2e  30446  avril1  30751  helloworld  30753  topnfbey  30757  xrge00  33271  axnulALT2  35411  axsepg3ALT  35474  fmlaomn0  35777  gonan0  35779  goaln0  35780  prv0  35817  dfon2lem7  36174  nandsym1  36818  bj-inftyexpitaudisj  37732  padd01  40470  ifpdfan  44079  sucomisnotcard  44157  clsk1indlem4  44657  iblempty  46566  salexct2  46940  0nodd  48819  2nodd  48821  1neven  48887  ipolub00  49651