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

Theorem go-comi 76
Description: Inference form of go-com 75 (Contributed by la korvo, 31-Jul-2023.)
Hypothesis
Ref Expression
go-comi.0go broda gi brode
Assertion
Ref Expression
go-comigo brode gi broda

Proof of Theorem go-comi
StepHypRef Expression
1 go-comi.0 . 2go broda gi brode
2 go-com-lem 74 . 2ganai go broda gi brode gi go brode gi broda
31, 2ax-mp 10 1go brode gi broda
Colors of variables: sumti selbri bridi
Syntax hints:  go bgo 60
This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 43  ax-ge-re 44  ax-ge-in 45
This theorem depends on definitions:  df-go 61
This theorem is referenced by:  bi-rev  80  bi-rev-syl  81  a-com  156  o-com  170  se-ganaii  189  se-ganair  190  ro2-bi-rev  211  du-symi  223  dunli-sym  333  mintu-sym  340  te-ganaii  367  te-ganair  368  subid  394
  Copyright terms: Public domain W3C validator