Theorem intnan 998

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

Syntax hints:  ¬ wn 3   ∧ wa 383

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 385

This theorem is referenced by:  bianfi  1004  indifdir  4027  axnulALT  4940  axnul  4941  cnv0  5694  imadif  6135  xrltnr  12167  nltmnf  12177  0nelfz1  12574  smu01  15431  3lcm2e6woprm  15551  6lcm4e12  15552  meet0  17359  join0  17360  zringndrg  20061  zclmncvs  23169  legso  25715  rgrx0ndm  26721  wwlksnext  27033  ntrl2v2e  27332  avril1  27652  helloworld  27654  topnfbey  27658  xrge00  30017  dfon2lem7  32021  nolt02o  32173  nandsym1  32749  subsym1  32754  padd01  35619  ifpdfan  38331  clsk1indlem4  38863  iblempty  40703  salexct2  41079  0nodd  42339  2nodd  42341  1neven  42461