intnan - Metamath Proof Explorer

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

Theorem intnan 912

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 459	. 2 $/\$
3	1, 2	mto 176	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3 $/\$ wa 367

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 369

This theorem is referenced by: bianfi 923 indifdir 3751 axnulALT 4566 axnul 4567 imadif 5645 xrltnr 11333 nltmnf 11341 smu01 14220 meet0 15966 join0 15967 legso 24186 wwlknext 24926 avril1 25373 helloworld 25375 xrge00 27908 dfon2lem7 29461 nandsym1 30115 subsym1 30120 iblempty 32003 0nodd 32870 2nodd 32872 1neven 32992 padd01 35932 ifpdfan 38134