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  4710  axnul  4711  imadif  5873  xrltnr  11793  nltmnf  11803  0nelfz1  12189  smu01  14995  3lcm2e6woprm  15115  6lcm4e12  15116  meet0  16909  join0  16910  legso  25240  wwlknext  26046  avril1  26505  helloworld  26507  topnfbey  26511  xrge00  28811  dfon2lem7  30732  nandsym1  31385  subsym1  31390  padd01  33909  ifpdfan  36623  clsk1indlem4  37156  iblempty  38651  salexct2  39027  rgrx0ndm  40785  wwlksnext  41091  ntrl2v2e  41317  0nodd  41592  2nodd  41594  1neven  41714