Theorem intnanr 960

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

Syntax hints:  ¬ wn 3   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  falantru  1505  rab0  3934  rab0OLD  3935  0nelxp  5108  co02  5611  xrltnr  11897  pnfnlt  11906  nltmnf  11907  0nelfz1  12299  smu02  15128  0g0  17179  axlowdimlem13  25729  axlowdimlem16  25732  axlowdim  25736  signstfvneq0  30421  bcneg1  31322  linedegen  31884  padd02  34564  eldioph4b  36841  iblempty  39475  notatnand  40354  fun2dmnopgexmpl  40588