Theorem intnanr 488

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

Syntax hints:  ¬ wn 3   ∧ wa 396

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 397

This theorem is referenced by:  falantru  1574  rab0  4316  0nelopab  5480  0nelxp  5623  co02  6164  xrltnr  12855  pnfnlt  12864  nltmnf  12865  0nelfz1  13275  smu02  16194  0g0  18348  axlowdimlem13  27322  axlowdimlem16  27325  axlowdim  27329  signstfvneq0  32551  gonanegoal  33314  gonan0  33354  goaln0  33355  fmla0disjsuc  33360  bcneg1  33702  nolt02o  33898  nogt01o  33899  linedegen  34445  epnsymrel  36676  padd02  37826  eldioph4b  40633  iblempty  43506  notatnand  44391  iota0ndef  44533  aiota0ndef  44589  fun2dmnopgexmpl  44776