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  4336  0nelopab  5540  0nelxp  5685  co02  6255  xrltnr  13229  pnfnlt  13238  nltmnf  13239  0nelfz1  13656  smu02  16637  0g0  18824  degenmgmnfn  19116  nolt02o  28034  nogt01o  28035  axlowdimlem13  29514  axlowdimlem16  29517  axlowdim  29521  signstfvneq0  35184  axsepg2  35781  axsepg4  35784  gonanegoal  36086  gonan0  36126  goaln0  36127  fmla0disjsuc  36132  bcneg1  36470  linedegen  36878  epnsymrel  39546  padd02  40837  eldioph4b  43771  iblempty  46919  notatnand  47910  iota0ndef  48053  aiota0ndef  48111  fun2dmnopgexmpl  48298