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 930

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

Colors of variables: wff setvar class

Syntax hints:

wn 3 $/\$ wa 375

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 190 df-an 377

This theorem is referenced by: bianfi 941 indifdir 3710 axnulALT 4544 axnul 4545 axnulOLD 4546 imadif 5679 xrltnr 11449 nltmnf 11459 0nelfz1 11846 smu01 14508 3lcm2e6woprm 14628 6lcm4e12 14629 meet0 16431 join0 16432 legso 24692 wwlknext 25500 avril1 25948 helloworld 25950 topnfbey 25954 xrge00 28496 dfon2lem7 30483 nandsym1 31130 subsym1 31135 padd01 33420 ifpdfan 36153 iblempty 37879 salexct2 38235 rgrx0ndm 39657 ntrl2v2e 39872 0nodd 40082 2nodd 40084 1neven 40204