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

---

Theorem go-ganai 85

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 84. (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 84	. 2 ⊢ ge ganai broda gi brode gi ganai brode gi broda
3	2	ge-lei 51	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 48

This theorem depends on definitions:  df-go 83

This theorem is referenced by:  bi  101  bi-rev-syl  103  sylbi  104  sylib  105  syl5bi  108  se-dual  217  se-dual-l  218  se-ganaii  220  se-ganair  221  ro2-bi  245  ro2-bi-rev  246  naku-uncur  274  te-dual  401  te-dual-l  402  te-ganaii  404  te-ganair  405  sub1  449  mapti-ckini  709

Copyright terms: Public domain

W3C validator