Theorem intnanr 999

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 474	. 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  1657  rab0  4098  rab0OLD  4099  0nelxp  5300  co02  5810  xrltnr  12146  pnfnlt  12155  nltmnf  12156  0nelfz1  12553  smu02  15411  0g0  17464  axlowdimlem13  26033  axlowdimlem16  26036  axlowdim  26040  signstfvneq0  30958  bcneg1  31929  nolt02o  32151  linedegen  32556  epnsymrel  34631  padd02  35601  eldioph4b  37877  iblempty  40684  notatnand  41569  fun2dmnopgexmpl  41811