Theorem intnanr 491

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)

Hypothesis

Ref	Expression
intnan.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
intnanr	⊢ ¬ (𝜑 ∧ 𝜓)

Proof of Theorem intnanr

Step	Hyp	Ref	Expression
1		intnan.1	. 2 ⊢ ¬ 𝜑
2		simpl 486	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	mto 200	1 ⊢ ¬ (𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  falantru  1573  rab0  4291  0nelxp  5553  co02  6080  xrltnr  12502  pnfnlt  12511  nltmnf  12512  0nelfz1  12921  smu02  15826  0g0  17866  axlowdimlem13  26748  axlowdimlem16  26751  axlowdim  26755  signstfvneq0  31952  gonanegoal  32712  gonan0  32752  goaln0  32753  fmla0disjsuc  32758  bcneg1  33081  nolt02o  33312  linedegen  33717  epnsymrel  35958  padd02  37108  eldioph4b  39752  iblempty  42607  notatnand  43489  iota0ndef  43631  aiota0ndef  43652  fun2dmnopgexmpl  43840