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  1577  rab0  4340  0nelopab  5521  0nelxp  5666  co02  6227  xrltnr  13045  pnfnlt  13054  nltmnf  13055  0nelfz1  13471  smu02  16426  0g0  18601  nolt02o  27675  nogt01o  27676  axlowdimlem13  29039  axlowdimlem16  29042  axlowdim  29046  signstfvneq0  34749  gonanegoal  35565  gonan0  35605  goaln0  35606  fmla0disjsuc  35611  bcneg1  35949  linedegen  36356  epnsymrel  38891  padd02  40182  eldioph4b  43162  iblempty  46317  notatnand  47250  iota0ndef  47393  aiota0ndef  47451  fun2dmnopgexmpl  47638