Theorem intnan 960

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 477	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 188	1 ⊢ ¬ (𝜓 ∧ 𝜑)

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 197  df-an 386

This theorem is referenced by:  bianfi  966  indifdir  3883  axnulALT  4787  axnul  4788  cnv0  5535  imadif  5973  xrltnr  11953  nltmnf  11963  0nelfz1  12360  smu01  15208  3lcm2e6woprm  15328  6lcm4e12  15329  meet0  17137  join0  17138  zringndrg  19838  zclmncvs  22948  legso  25494  rgrx0ndm  26489  wwlksnext  26788  ntrl2v2e  27018  avril1  27319  helloworld  27321  topnfbey  27325  xrge00  29686  dfon2lem7  31694  nolt02o  31845  nandsym1  32421  subsym1  32426  padd01  35097  ifpdfan  37810  clsk1indlem4  38342  iblempty  40181  salexct2  40557  0nodd  41810  2nodd  41812  1neven  41932