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  4349  0nelopab  5527  0nelxp  5672  co02  6233  xrltnr  13079  pnfnlt  13088  nltmnf  13089  0nelfz1  13504  smu02  16457  0g0  18591  nolt02o  27607  nogt01o  27608  axlowdimlem13  28881  axlowdimlem16  28884  axlowdim  28888  signstfvneq0  34563  gonanegoal  35339  gonan0  35379  goaln0  35380  fmla0disjsuc  35385  bcneg1  35723  linedegen  36131  epnsymrel  38553  padd02  39806  eldioph4b  42799  iblempty  45963  notatnand  46897  iota0ndef  47040  aiota0ndef  47098  fun2dmnopgexmpl  47285