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  1575  rab0  4386  0nelopab  5572  0nelxp  5719  co02  6280  xrltnr  13161  pnfnlt  13170  nltmnf  13171  0nelfz1  13583  smu02  16524  0g0  18677  nolt02o  27740  nogt01o  27741  axlowdimlem13  28969  axlowdimlem16  28972  axlowdim  28976  signstfvneq0  34587  gonanegoal  35357  gonan0  35397  goaln0  35398  fmla0disjsuc  35403  bcneg1  35736  linedegen  36144  epnsymrel  38563  padd02  39814  eldioph4b  42822  iblempty  45980  notatnand  46908  iota0ndef  47051  aiota0ndef  47109  fun2dmnopgexmpl  47296