Theorem intnanr 961

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  1508  rab0  3955  rab0OLD  3956  0nelxp  5143  co02  5649  xrltnr  11953  pnfnlt  11962  nltmnf  11963  0nelfz1  12360  smu02  15209  0g0  17263  axlowdimlem13  25834  axlowdimlem16  25837  axlowdim  25841  signstfvneq0  30649  bcneg1  31622  nolt02o  31845  linedegen  32250  padd02  35098  eldioph4b  37375  iblempty  40181  notatnand  41063  fun2dmnopgexmpl  41303