Theorem intnanr 492

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

Syntax hints:  ¬ wn 3   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  falantru  1605  rab0OLD  4344  0nelopab  5552  0nelxp  5697  co02  6264  xrltnr  13145  pnfnlt  13154  nltmnf  13155  0nelfz1  13572  smu02  16546  0g0  18723  nolt02o  27837  nogt01o  27838  axlowdimlem13  29282  axlowdimlem16  29285  axlowdim  29289  signstfvneq0  34937  axsepg2  35531  axsepg4  35534  gonanegoal  35822  gonan0  35862  goaln0  35863  fmla0disjsuc  35868  bcneg1  36206  linedegen  36613  epnsymrel  39273  padd02  40564  eldioph4b  43518  iblempty  46659  notatnand  47610  iota0ndef  47753  aiota0ndef  47811  fun2dmnopgexmpl  47998