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  1605  rab0OLD  4339  0nelopab  5548  0nelxp  5693  co02  6261  xrltnr  13174  pnfnlt  13183  nltmnf  13184  0nelfz1  13601  smu02  16583  0g0  18763  degenmgmnfn  19055  nolt02o  27939  nogt01o  27940  axlowdimlem13  29419  axlowdimlem16  29422  axlowdim  29426  signstfvneq0  35088  axsepg2  35674  axsepg4  35677  gonanegoal  35939  gonan0  35979  goaln0  35980  fmla0disjsuc  35985  bcneg1  36323  linedegen  36731  epnsymrel  39402  padd02  40693  eldioph4b  43660  iblempty  46801  notatnand  47792  iota0ndef  47935  aiota0ndef  47993  fun2dmnopgexmpl  48180