Theorem intnanr 488

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

Syntax hints:  ¬ wn 3   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  falantru  1582  rab0  4321  0nelopab  5514  0nelxp  5659  co02  6219  xrltnr  13068  pnfnlt  13077  nltmnf  13078  0nelfz1  13495  smu02  16454  0g0  18630  nolt02o  27684  nogt01o  27685  axlowdimlem13  29048  axlowdimlem16  29051  axlowdim  29055  signstfvneq0  34763  axsepg2  35328  axsepg4  35331  gonanegoal  35587  gonan0  35627  goaln0  35628  fmla0disjsuc  35633  bcneg1  35971  linedegen  36378  epnsymrel  39020  padd02  40311  eldioph4b  43263  iblempty  46415  notatnand  47366  iota0ndef  47509  aiota0ndef  47567  fun2dmnopgexmpl  47754