Theorem intnanr 487

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

Syntax hints:  ¬ wn 3   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  falantru  1575  rab0  4339  0nelopab  5512  0nelxp  5657  co02  6213  xrltnr  13039  pnfnlt  13048  nltmnf  13049  0nelfz1  13464  smu02  16416  0g0  18556  nolt02o  27623  nogt01o  27624  axlowdimlem13  28917  axlowdimlem16  28920  axlowdim  28924  signstfvneq0  34539  gonanegoal  35324  gonan0  35364  goaln0  35365  fmla0disjsuc  35370  bcneg1  35708  linedegen  36116  epnsymrel  38538  padd02  39791  eldioph4b  42784  iblempty  45947  notatnand  46881  iota0ndef  47024  aiota0ndef  47082  fun2dmnopgexmpl  47269