Theorem intnanr 486

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

Syntax hints:  ¬ wn 3   ∧ wa 394

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 395

This theorem is referenced by:  falantru  1568  rab0  4384  0nelopab  5571  0nelxp  5714  co02  6267  xrltnr  13137  pnfnlt  13146  nltmnf  13147  0nelfz1  13558  smu02  16467  0g0  18629  nolt02o  27646  nogt01o  27647  axlowdimlem13  28783  axlowdimlem16  28786  axlowdim  28790  signstfvneq0  34209  gonanegoal  34967  gonan0  35007  goaln0  35008  fmla0disjsuc  35013  bcneg1  35335  linedegen  35744  epnsymrel  38038  padd02  39289  eldioph4b  42234  iblempty  45355  notatnand  46280  iota0ndef  46423  aiota0ndef  46479  fun2dmnopgexmpl  46666