Theorem intnanr 486

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

Syntax hints:  ¬ wn 3   ∧ wa 394

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 395

This theorem is referenced by:  falantru  1574  rab0  4381  0nelopab  5566  0nelxp  5709  co02  6258  xrltnr  13103  pnfnlt  13112  nltmnf  13113  0nelfz1  13524  smu02  16432  0g0  18589  nolt02o  27434  nogt01o  27435  axlowdimlem13  28479  axlowdimlem16  28482  axlowdim  28486  signstfvneq0  33881  gonanegoal  34641  gonan0  34681  goaln0  34682  fmla0disjsuc  34687  bcneg1  35010  linedegen  35419  epnsymrel  37735  padd02  38986  eldioph4b  41851  iblempty  44979  notatnand  45904  iota0ndef  46047  aiota0ndef  46103  fun2dmnopgexmpl  46290