Theorem intnanr 488

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

Syntax hints:  ¬ wn 3   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  falantru  1577  rab0  4322  0nelopab  5480  0nelxp  5623  co02  6162  xrltnr  12852  pnfnlt  12861  nltmnf  12862  0nelfz1  13272  smu02  16190  0g0  18344  axlowdimlem13  27318  axlowdimlem16  27321  axlowdim  27325  signstfvneq0  32545  gonanegoal  33308  gonan0  33348  goaln0  33349  fmla0disjsuc  33354  bcneg1  33696  nolt02o  33892  nogt01o  33893  linedegen  34439  epnsymrel  36670  padd02  37820  eldioph4b  40628  iblempty  43475  notatnand  44357  iota0ndef  44499  aiota0ndef  44555  fun2dmnopgexmpl  44742