Theorem intnanr 491

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

Syntax hints:  ¬ wn 3   ∧ wa 399

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 400

This theorem is referenced by:  falantru  1594  rab0OLD  4339  0nelopab  5534  0nelxp  5679  co02  6244  xrltnr  13118  pnfnlt  13127  nltmnf  13128  0nelfz1  13545  smu02  16504  0g0  18681  nolt02o  27736  nogt01o  27737  axlowdimlem13  29101  axlowdimlem16  29104  axlowdim  29108  signstfvneq0  34830  axsepg2  35400  axsepg4  35403  gonanegoal  35666  gonan0  35706  goaln0  35707  fmla0disjsuc  35712  bcneg1  36050  linedegen  36457  epnsymrel  39109  padd02  40400  eldioph4b  43352  iblempty  46503  notatnand  47454  iota0ndef  47597  aiota0ndef  47655  fun2dmnopgexmpl  47842