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  1576  rab0  4347  0nelopab  5529  0nelxp  5672  co02  6217  xrltnr  13049  pnfnlt  13058  nltmnf  13059  0nelfz1  13470  smu02  16378  0g0  18533  nolt02o  27080  nogt01o  27081  axlowdimlem13  27966  axlowdimlem16  27969  axlowdim  27973  signstfvneq0  33273  gonanegoal  34033  gonan0  34073  goaln0  34074  fmla0disjsuc  34079  bcneg1  34395  linedegen  34804  epnsymrel  37097  padd02  38348  eldioph4b  41192  iblempty  44326  notatnand  45251  iota0ndef  45393  aiota0ndef  45449  fun2dmnopgexmpl  45636