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 196	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 206  df-an 397

This theorem is referenced by:  falantru  1576  rab0  4382  0nelopab  5567  0nelxp  5710  co02  6259  xrltnr  13103  pnfnlt  13112  nltmnf  13113  0nelfz1  13524  smu02  16432  0g0  18589  nolt02o  27422  nogt01o  27423  axlowdimlem13  28467  axlowdimlem16  28470  axlowdim  28474  signstfvneq0  33869  gonanegoal  34629  gonan0  34669  goaln0  34670  fmla0disjsuc  34675  bcneg1  34998  linedegen  35407  epnsymrel  37735  padd02  38986  eldioph4b  41851  iblempty  44980  notatnand  45905  iota0ndef  46048  aiota0ndef  46104  fun2dmnopgexmpl  46291