Theorem intnanr 493

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

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  falantru  1605  rab0OLD  4339  0nelopab  5544  0nelxp  5689  co02  6277  xrltnr  13275  pnfnlt  13284  nltmnf  13285  0nelfz1  13703  smu02  16686  0g0  18873  degenmgmnfn  19165  nolt02o  28082  nogt01o  28083  axlowdimlem13  29562  axlowdimlem16  29565  axlowdim  29569  signstfvneq0  35271  axsepg2  35908  axsepg4  35911  gonanegoal  36284  gonan0  36324  goaln0  36325  fmla0disjsuc  36330  bcneg1  36679  linedegen  37086  epnsymrel  39770  padd02  41061  eldioph4b  44011  iblempty  47180  notatnand  48171  iota0ndef  48314  aiota0ndef  48372  fun2dmnopgexmpl  48559  par2hom  50984