Theorem intnanr 981

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 472	. 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 197  df-an 385

This theorem is referenced by:  falantru  1548  rab0  3988  rab0OLD  3989  0nelxp  5177  co02  5687  xrltnr  11991  pnfnlt  12000  nltmnf  12001  0nelfz1  12398  smu02  15256  0g0  17310  axlowdimlem13  25879  axlowdimlem16  25882  axlowdim  25886  signstfvneq0  30777  bcneg1  31748  nolt02o  31970  linedegen  32375  padd02  35416  eldioph4b  37692  iblempty  40499  notatnand  41384  fun2dmnopgexmpl  41626