intnan - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > intnan		Structured version Unicode version

Theorem intnan 905

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 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3 $/\$ wa 369

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

This theorem is referenced by: bianfi 916 indifdir 3706 axnulALT 4519 axnul 4520 imadif 5593 xrltnr 11204 nltmnf 11212 smu01 13786 meet0 15411 join0 15412 avril1 23793 helloworld 23795 xrge00 26283 dfon2lem7 27738 nandsym1 28404 subsym1 28409 wwlknext 30496 padd01 33763