nomei-gaiho - brismu bridi

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

Theorem nomei-gaiho 251

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 250	. 2 ⊢ naku zo'u ko'a cmima le nomei ku
2		nomei-gaiho.0	. 2 ⊢ ko'a cmima le nomei ku
3	1, 2	nakuii 216	1 ⊢ gai'o

Colors of variables: sumti selbri bridi

Syntax hints: cmima sbcmima 246 le snomei 249

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

This theorem depends on definitions: df-go 52 df-naku 211 df-nomei 250

This theorem is referenced by: (None)