Theorem intnan 959

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  965  indifdir  3865  axnulALT  4757  axnul  4758  cnv0  5504  imadif  5941  xrltnr  11913  nltmnf  11923  0nelfz1  12318  smu01  15151  3lcm2e6woprm  15271  6lcm4e12  15272  meet0  17077  join0  17078  zringndrg  19778  zclmncvs  22888  legso  25428  rgrx0ndm  26393  wwlksnext  26691  ntrl2v2e  26918  avril1  27207  helloworld  27209  topnfbey  27213  xrge00  29513  dfon2lem7  31448  nandsym1  32116  subsym1  32121  padd01  34616  ifpdfan  37330  clsk1indlem4  37863  iblempty  39518  salexct2  39894  0nodd  41128  2nodd  41130  1neven  41250