Theorem intnanr 476

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

Syntax hints:  ¬ wn 3   ∧ wa 383

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 198  df-an 384

This theorem is referenced by:  falantru  1659  rab0  4113  0nelxp  5296  co02  5804  xrltnr  12175  pnfnlt  12184  nltmnf  12185  0nelfz1  12589  smu02  15438  0g0  17491  axlowdimlem13  26076  axlowdimlem16  26079  axlowdim  26083  signstfvneq0  31006  bcneg1  31977  nolt02o  32199  linedegen  32604  epnsymrel  34665  padd02  35636  eldioph4b  37916  iblempty  40704  notatnand  41589  iota0ndef  41698  aiota0ndef  41712  fun2dmnopgexmpl  41850