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  1571  rab0  4391  0nelopab  5576  0nelxp  5722  co02  6281  xrltnr  13158  pnfnlt  13167  nltmnf  13168  0nelfz1  13579  smu02  16520  0g0  18689  nolt02o  27754  nogt01o  27755  axlowdimlem13  28983  axlowdimlem16  28986  axlowdim  28990  signstfvneq0  34565  gonanegoal  35336  gonan0  35376  goaln0  35377  fmla0disjsuc  35382  bcneg1  35715  linedegen  36124  epnsymrel  38543  padd02  39794  eldioph4b  42798  iblempty  45920  notatnand  46845  iota0ndef  46988  aiota0ndef  47046  fun2dmnopgexmpl  47233