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  4326  0nelopab  5520  0nelxp  5665  co02  6225  xrltnr  13070  pnfnlt  13079  nltmnf  13080  0nelfz1  13497  smu02  16456  0g0  18632  nolt02o  27659  nogt01o  27660  axlowdimlem13  29023  axlowdimlem16  29026  axlowdim  29030  signstfvneq0  34716  gonanegoal  35534  gonan0  35574  goaln0  35575  fmla0disjsuc  35580  bcneg1  35918  linedegen  36325  epnsymrel  38967  padd02  40258  eldioph4b  43239  iblempty  46393  notatnand  47344  iota0ndef  47487  aiota0ndef  47545  fun2dmnopgexmpl  47732