Theorem intnan 951

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 476	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 187	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 196  df-an 385

This theorem is referenced by:  bianfi  962  indifdir  3842  axnulALT  4715  axnul  4716  cnv0  5454  imadif  5887  xrltnr  11829  nltmnf  11839  0nelfz1  12231  smu01  15046  3lcm2e6woprm  15166  6lcm4e12  15167  meet0  16960  join0  16961  zringndrg  19657  zclmncvs  22756  legso  25294  wwlknext  26252  avril1  26711  helloworld  26713  topnfbey  26717  xrge00  29017  dfon2lem7  30938  nandsym1  31591  subsym1  31596  padd01  34115  ifpdfan  36829  clsk1indlem4  37362  iblempty  38857  salexct2  39233  rgrx0ndm  40793  wwlksnext  41099  ntrl2v2e  41325  0nodd  41600  2nodd  41602  1neven  41722