nomei-gaiho - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > nomei-gaiho

Theorem nomei-gaiho 326

Description: If the empty set is inhabited, then there is a contradiction. (Contributed by la korvo, 16-May-2024.)

**Hypothesis**
Ref	Expression
nomei-gaiho.0	⊢ ko'a cmima le nomei ku

**Assertion**
Ref	Expression
nomei-gaiho	⊢ gai'o

**Proof of Theorem nomei-gaiho**
Step	Hyp	Ref	Expression
1		df-nomei 325	. 2 ⊢ naku ko'a cmima le nomei ku
2		nomei-gaiho.0	. 2 ⊢ ko'a cmima le nomei ku
3	1, 2	nakuii 279	1 ⊢ gai'o

Colors of variables: sumti selbri bridi

Syntax hints: cmima sbcmima 320 le snomei 324

This theorem was proved from axioms: ax-mp 10 ax-ge-le 48

This theorem depends on definitions: df-go 83 df-naku 274 df-nomei 325

This theorem is referenced by: (None)