nomei-gaiho - brismu bridi

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

Theorem nomei-gaiho 288

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

Colors of variables: sumti selbri bridi

Syntax hints: cmima sbcmima 282 le snomei 286

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

This theorem depends on definitions: df-go 61 df-naku 237 df-nomei 287

This theorem is referenced by: (None)