stewart - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > stewart

Theorem stewart 259

Description: A syllogism underlying the Swallowing Elephants puzzle from chapter 4 of [Stewart] p. 22. (Contributed by la korvo, 1-Jan-2025.)

**Assertion**
Ref	Expression
stewart	⊢ ganai broda gi naku brodu

**Proof of Theorem stewart**
Step	Hyp	Ref	Expression
1		stewart.0	. . 3 ⊢ ganai broda gi brode
2		stewart.3	. . 3 ⊢ ganai brode gi naku brodo
3	1, 2	syl 20	. 2 ⊢ ganai broda gi naku brodo
4		stewart.2	. . 3 ⊢ ganai brodu gi brodi
5		stewart.1	. . 3 ⊢ ganai brodi gi brodo
6	4, 5	syl 20	. 2 ⊢ ganai brodu gi brodo
7	3, 6	nsyl 258	1 ⊢ ganai broda gi naku brodu

Colors of variables: sumti selbri bridi

Syntax hints: naku bnk 236

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-sdo 245 ax-efq 248

This theorem is referenced by: (None)