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 196	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 206  df-an 396

This theorem is referenced by:  falantru  1574  rab0  4313  0nelopab  5471  0nelxp  5614  co02  6153  xrltnr  12784  pnfnlt  12793  nltmnf  12794  0nelfz1  13204  smu02  16122  0g0  18263  axlowdimlem13  27225  axlowdimlem16  27228  axlowdim  27232  signstfvneq0  32451  gonanegoal  33214  gonan0  33254  goaln0  33255  fmla0disjsuc  33260  bcneg1  33608  nolt02o  33825  nogt01o  33826  linedegen  34372  epnsymrel  36603  padd02  37753  eldioph4b  40549  iblempty  43396  notatnand  44278  iota0ndef  44420  aiota0ndef  44476  fun2dmnopgexmpl  44663