Theorem intnan 914

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
intnan.1

Assertion

Ref	Expression
intnan

Proof of Theorem intnan

Step	Hyp	Ref	Expression
1		intnan.1	. 2
2		simpr 461	. 2
3	1, 2	mto 176	1

Syntax hints:  -.wn 3  /\wa 369

This theorem is referenced by:  bianfi  925  indifdir  3753  axnulALT  4579  axnul  4580  imadif  5668  xrltnr  11359  nltmnf  11367  smu01  14136  meet0  15767  join0  15768  legso  23985  wwlknext  24724  avril1  25171  helloworld  25173  xrge00  27674  dfon2lem7  29221  nandsym1  29887  subsym1  29892  iblempty  31764  0nodd  32498  2nodd  32500  1neven  32738  padd01  35535  bj-ifdfan  37727

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