Theorem intnanr 490

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

Syntax hints:  ¬ wn 3   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  falantru  1568  rab0  4337  0nelxp  5584  co02  6108  xrltnr  12508  pnfnlt  12517  nltmnf  12518  0nelfz1  12920  smu02  15830  0g0  17868  axlowdimlem13  26734  axlowdimlem16  26737  axlowdim  26741  signstfvneq0  31837  gonanegoal  32594  gonan0  32634  goaln0  32635  fmla0disjsuc  32640  bcneg1  32963  nolt02o  33194  linedegen  33599  epnsymrel  35792  padd02  36942  eldioph4b  39401  iblempty  42242  notatnand  43125  iota0ndef  43267  aiota0ndef  43288  fun2dmnopgexmpl  43476