Theorem intnanr 483

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

Syntax hints:  ¬ wn 3   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  falantru  1692  rab0  4187  0nelxp  5380  co02  5894  xrltnr  12246  pnfnlt  12255  nltmnf  12256  0nelfz1  12660  smu02  15589  0g0  17623  axlowdimlem13  26260  axlowdimlem16  26263  axlowdim  26267  signstfvneq0  31193  bcneg1  32160  nolt02o  32379  linedegen  32784  epnsymrel  34851  padd02  35882  eldioph4b  38214  iblempty  40969  notatnand  41851  iota0ndef  41964  aiota0ndef  41986  fun2dmnopgexmpl  42181