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  1574  rab0  4366  0nelopab  5552  0nelxp  5699  co02  6260  xrltnr  13143  pnfnlt  13152  nltmnf  13153  0nelfz1  13565  smu02  16506  0g0  18646  nolt02o  27676  nogt01o  27677  axlowdimlem13  28899  axlowdimlem16  28902  axlowdim  28906  signstfvneq0  34546  gonanegoal  35316  gonan0  35356  goaln0  35357  fmla0disjsuc  35362  bcneg1  35695  linedegen  36103  epnsymrel  38522  padd02  39773  eldioph4b  42785  iblempty  45937  notatnand  46866  iota0ndef  47009  aiota0ndef  47067  fun2dmnopgexmpl  47254