Theorem intnanr 492

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

Syntax hints:  ¬ wn 3   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  falantru  1598  rab0OLD  4343  0nelopab  5541  0nelxp  5686  co02  6252  xrltnr  13135  pnfnlt  13144  nltmnf  13145  0nelfz1  13562  smu02  16535  0g0  18712  nolt02o  27817  nogt01o  27818  axlowdimlem13  29213  axlowdimlem16  29216  axlowdim  29220  signstfvneq0  34876  axsepg2  35448  axsepg4  35451  gonanegoal  35715  gonan0  35755  goaln0  35756  fmla0disjsuc  35761  bcneg1  36099  linedegen  36506  epnsymrel  39157  padd02  40448  eldioph4b  43400  iblempty  46537  notatnand  47488  iota0ndef  47631  aiota0ndef  47689  fun2dmnopgexmpl  47876