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  4361  0nelopab  5542  0nelxp  5688  co02  6249  xrltnr  13135  pnfnlt  13144  nltmnf  13145  0nelfz1  13560  smu02  16506  0g0  18642  nolt02o  27659  nogt01o  27660  axlowdimlem13  28933  axlowdimlem16  28936  axlowdim  28940  signstfvneq0  34604  gonanegoal  35374  gonan0  35414  goaln0  35415  fmla0disjsuc  35420  bcneg1  35753  linedegen  36161  epnsymrel  38580  padd02  39831  eldioph4b  42834  iblempty  45994  notatnand  46925  iota0ndef  47068  aiota0ndef  47126  fun2dmnopgexmpl  47313