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  1576  rab0  4338  0nelopab  5513  0nelxp  5658  co02  6219  xrltnr  13033  pnfnlt  13042  nltmnf  13043  0nelfz1  13459  smu02  16414  0g0  18589  nolt02o  27663  nogt01o  27664  axlowdimlem13  29027  axlowdimlem16  29030  axlowdim  29034  signstfvneq0  34729  gonanegoal  35546  gonan0  35586  goaln0  35587  fmla0disjsuc  35592  bcneg1  35930  linedegen  36337  epnsymrel  38815  padd02  40068  eldioph4b  43049  iblempty  46205  notatnand  47138  iota0ndef  47281  aiota0ndef  47339  fun2dmnopgexmpl  47526