Theorem intnanr 493

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

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  falantru  1604  rab0OLD  4335  0nelopab  5539  0nelxp  5684  co02  6262  xrltnr  13251  pnfnlt  13260  nltmnf  13261  0nelfz1  13679  smu02  16662  0g0  18849  degenmgmnfn  19141  nolt02o  28057  nogt01o  28058  axlowdimlem13  29537  axlowdimlem16  29540  axlowdim  29544  signstfvneq0  35247  axsepg2  35864  axsepg4  35867  gonanegoal  36203  gonan0  36243  goaln0  36244  fmla0disjsuc  36249  bcneg1  36593  linedegen  37000  epnsymrel  39671  padd02  40962  eldioph4b  43911  iblempty  47068  notatnand  48059  iota0ndef  48202  aiota0ndef  48260  fun2dmnopgexmpl  48447  par2hom  50872