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  4335  0nelopab  5508  0nelxp  5653  co02  6213  xrltnr  13020  pnfnlt  13029  nltmnf  13030  0nelfz1  13445  smu02  16400  0g0  18574  nolt02o  27635  nogt01o  27636  axlowdimlem13  28934  axlowdimlem16  28937  axlowdim  28941  signstfvneq0  34606  gonanegoal  35417  gonan0  35457  goaln0  35458  fmla0disjsuc  35463  bcneg1  35801  linedegen  36208  epnsymrel  38678  padd02  39931  eldioph4b  42928  iblempty  46087  notatnand  47020  iota0ndef  47163  aiota0ndef  47221  fun2dmnopgexmpl  47408