intnan - Metamath Proof Explorer

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

Theorem intnan 960

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

Colors of variables: wff setvar class

Syntax hints:

wn 3 $/\$ wa 384

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 386

This theorem is referenced by: bianfi 966 indifdir 3883 axnulALT 4787 axnul 4788 cnv0 5535 imadif 5973 xrltnr 11953 nltmnf 11963 0nelfz1 12360 smu01 15208 3lcm2e6woprm 15328 6lcm4e12 15329 meet0 17137 join0 17138 zringndrg 19838 zclmncvs 22948 legso 25494 rgrx0ndm 26489 wwlksnext 26788 ntrl2v2e 27018 avril1 27319 helloworld 27321 topnfbey 27325 xrge00 29686 dfon2lem7 31694 nolt02o 31845 nandsym1 32421 subsym1 32426 padd01 35097 ifpdfan 37810 clsk1indlem4 38342 iblempty 40181 salexct2 40557 0nodd 41810 2nodd 41812 1neven 41932