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

Theorem gripaui 296
Description: Inference form of df-gripau 295 (Contributed by la korvo, 15-Jul-2024.)
Hypothesis
Ref Expression
gripaui.0ko'a gripau ko'e
Assertion
Ref Expression
gripauiko'i cmima ko'a na.a ko'e

Proof of Theorem gripaui
StepHypRef Expression
1 gripaui.0 . 2ko'a gripau ko'e
2 df-gripau 295 . 2go ko'a gripau ko'e gi ko'i cmima ko'a na.a ko'e
31, 2bi 79 1ko'i cmima ko'a na.a ko'e
Colors of variables: sumti selbri bridi
Syntax hints:  na.a sjnaa 87  cmima sbcmima 282  gripau sbgripau 294
This theorem was proved from axioms:  ax-mp 10  ax-ge-le 43
This theorem depends on definitions:  df-go 61  df-gripau 295
This theorem is referenced by:  gripauis  298
  Copyright terms: Public domain W3C validator