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  1576  rab0  4336  0nelopab  5505  0nelxp  5650  co02  6208  xrltnr  13015  pnfnlt  13024  nltmnf  13025  0nelfz1  13440  smu02  16395  0g0  18569  nolt02o  27632  nogt01o  27633  axlowdimlem13  28930  axlowdimlem16  28933  axlowdim  28937  signstfvneq0  34580  gonanegoal  35384  gonan0  35424  goaln0  35425  fmla0disjsuc  35430  bcneg1  35768  linedegen  36176  epnsymrel  38598  padd02  39850  eldioph4b  42843  iblempty  46002  notatnand  46926  iota0ndef  47069  aiota0ndef  47127  fun2dmnopgexmpl  47314