intnan - Metamath Proof Explorer

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

Theorem intnan 923

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

Colors of variables: wff setvar class

Syntax hints:

wn 3 $/\$ wa 371

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 189 df-an 373

This theorem is referenced by: bianfi 934 indifdir 3730 axnulALT 4550 axnul 4551 axnulOLD 4552 imadif 5674 xrltnr 11423 nltmnf 11433 0nelfz1 11820 smu01 14453 3lcm2e6woprm 14573 6lcm4e12 14574 meet0 16376 join0 16377 legso 24636 wwlknext 25444 avril1 25892 helloworld 25894 topnfbey 25898 xrge00 28449 dfon2lem7 30436 nandsym1 31081 subsym1 31086 padd01 33301 ifpdfan 36035 iblempty 37668 0nodd 39114 2nodd 39116 1neven 39236