syl - brismu bridi

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

Theorem syl 18

Description: The quintessential syllogism. This inference is a standard workhorse for producing deductive forms. In terms of category theory, it composes arrows. (Contributed by la korvo, 30-Jul-2023.)

**Hypotheses**
Ref	Expression
syl.0	⊢ ganai broda gi brode
syl.1	⊢ ganai brode gi brodi

**Assertion**
Ref	Expression
syl	⊢ ganai broda gi brodi

**Proof of Theorem syl**
Step	Hyp	Ref	Expression
1		syl.0	. 2 ⊢ ganai broda gi brode
2		syl.1	. . 3 ⊢ ganai brode gi brodi
3	2	ki 12	. 2 ⊢ ganai broda gi ganai brode gi brodi
4	1, 3	mpd 16	1 ⊢ ganai broda gi brodi

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 14

This theorem is referenced by: sd 19 sylcom 21 kd 24 syl2im 28 ge-led 38 ge-red 40 sylbi 72 sylib 73 sylibr 74 se-dual 172 se-dual-l 173 se-dual-r 174 se-ganaii 175 se-ganair 176 gripau-trans 265 te-dual 327 te-dual-l 328 te-dual-r 329 te-ganaii 330 te-ganair 331 mapti-ckini 581

W3C validator