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  4346  0nelopab  5555  0nelxp  5700  co02  6267  xrltnr  13162  pnfnlt  13171  nltmnf  13172  0nelfz1  13589  smu02  16570  0g0  18747  nolt02o  27896  nogt01o  27897  axlowdimlem13  29341  axlowdimlem16  29344  axlowdim  29348  signstfvneq0  34991  axsepg2  35577  axsepg4  35580  gonanegoal  35865  gonan0  35905  goaln0  35906  fmla0disjsuc  35911  bcneg1  36249  linedegen  36656  epnsymrel  39336  padd02  40627  eldioph4b  43579  iblempty  46720  notatnand  47674  iota0ndef  47817  aiota0ndef  47875  fun2dmnopgexmpl  48062