Theorem intnanr 487

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

Syntax hints:  ¬ wn 3   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  falantru  1577  rab0  4327  0nelopab  5513  0nelxp  5658  co02  6219  xrltnr  13061  pnfnlt  13070  nltmnf  13071  0nelfz1  13488  smu02  16447  0g0  18623  nolt02o  27673  nogt01o  27674  axlowdimlem13  29037  axlowdimlem16  29040  axlowdim  29044  signstfvneq0  34732  gonanegoal  35550  gonan0  35590  goaln0  35591  fmla0disjsuc  35596  bcneg1  35934  linedegen  36341  epnsymrel  38981  padd02  40272  eldioph4b  43257  iblempty  46411  notatnand  47356  iota0ndef  47499  aiota0ndef  47557  fun2dmnopgexmpl  47744