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  4336  0nelxp  5588  co02  6112  xrltnr  12513  pnfnlt  12522  nltmnf  12523  0nelfz1  12925  smu02  15835  0g0  17873  axlowdimlem13  26739  axlowdimlem16  26742  axlowdim  26746  signstfvneq0  31842  gonanegoal  32599  gonan0  32639  goaln0  32640  fmla0disjsuc  32645  bcneg1  32968  nolt02o  33199  linedegen  33604  epnsymrel  35797  padd02  36947  eldioph4b  39406  iblempty  42248  notatnand  43131  iota0ndef  43273  aiota0ndef  43294  fun2dmnopgexmpl  43482