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  4346  0nelopab  5553  0nelxp  5698  co02  6265  xrltnr  13154  pnfnlt  13163  nltmnf  13164  0nelfz1  13581  smu02  16555  0g0  18732  nolt02o  27874  nogt01o  27875  axlowdimlem13  29319  axlowdimlem16  29322  axlowdim  29326  signstfvneq0  34972  axsepg2  35565  axsepg4  35568  gonanegoal  35856  gonan0  35896  goaln0  35897  fmla0disjsuc  35902  bcneg1  36240  linedegen  36647  epnsymrel  39327  padd02  40618  eldioph4b  43570  iblempty  46711  notatnand  47665  iota0ndef  47808  aiota0ndef  47866  fun2dmnopgexmpl  48053