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  1572  rab0  4409  0nelopab  5586  0nelxp  5734  co02  6291  xrltnr  13182  pnfnlt  13191  nltmnf  13192  0nelfz1  13603  smu02  16533  0g0  18702  nolt02o  27758  nogt01o  27759  axlowdimlem13  28987  axlowdimlem16  28990  axlowdim  28994  signstfvneq0  34549  gonanegoal  35320  gonan0  35360  goaln0  35361  fmla0disjsuc  35366  bcneg1  35698  linedegen  36107  epnsymrel  38518  padd02  39769  eldioph4b  42767  iblempty  45886  notatnand  46811  iota0ndef  46954  aiota0ndef  47012  fun2dmnopgexmpl  47199