brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  go-ganai

---

Theorem go-ganai 63

Description: Biconditional implication may be weakened to unidirectional implication. Category-theoretically, this theorem embeds the core of Loj. Inference form of left side of goli 62. (Contributed by la korvo, 17-Jul-2023.) (Shortened by la korvo, 29-Jul-2023.)

Hypothesis

Ref	Expression
go-ganai.0	⊢ go broda gi brode

Assertion

Ref	Expression
go-ganai	⊢ ganai broda gi brode

---

Proof of Theorem go-ganai

Step	Hyp	Ref	Expression
1		go-ganai.0	. . 3 ⊢ go broda gi brode
2	1	goli 62	. 2 ⊢ ge ganai broda gi brode gi ganai brode gi broda
3	2	ge-lei 46	1 ⊢ ganai broda gi brode

Colors of variables: sumti selbri bridi

Syntax hints:  ganai bgan 9

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

This theorem depends on definitions:  df-go 61

This theorem is referenced by:  bi  79  bi-rev-syl  81  sylbi  82  sylib  83  syl5bi  86  se-dual  186  se-dual-l  187  se-ganaii  189  se-ganair  190  ro2-bi  210  ro2-bi-rev  211  naku-uncur  238  te-dual  364  te-dual-l  365  te-ganaii  367  te-ganair  368  sub1  391  mapti-ckini  634

Copyright terms: Public domain

W3C validator