Theorem intnanr 952

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 187	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 196  df-an 385

This theorem is referenced by:  falantru  1499  rab0  3909  rab0OLD  3910  0nelxp  5067  co02  5566  xrltnr  11829  pnfnlt  11838  nltmnf  11839  0nelfz1  12231  smu02  15047  0g0  17086  axlowdimlem13  25634  axlowdimlem16  25637  axlowdim  25641  rusgra0edg  26482  signstfvneq0  29975  bcneg1  30875  linedegen  31420  padd02  34116  eldioph4b  36393  iblempty  38857  notatnand  39712  fun2dmnopgexmpl  40329