Theorem intnanr 915

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 457	. 2
3	1, 2	mto 176	1

Syntax hints:  -.wn 3  /\wa 369

This theorem is referenced by:  falantru  1421  rab0  3806  co02  5526  xrltnr  11359  pnfnlt  11366  nltmnf  11367  smu02  14137  0g0  15890  axlowdimlem13  24257  axlowdimlem16  24260  axlowdim  24264  rusgra0edg  24955  signstfvneq0  28529  linedegen  29793  eldioph4b  30745  iblempty  31764  notatnand  32091  padd02  35536

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 185  df-an 371