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

Theorem jonairi 310
Description: Reverse inference form of df-jonai 308 (Contributed by la korvo, 16-Aug-2023.)
Hypothesis
Ref Expression
jonairi.0gonai ko'a bu'a ko'e gi ko'a bu'e ko'e
Assertion
Ref Expression
jonairiko'a bu'a jonai bu'e ko'e
Distinct variable group:   bu'a , bu'e

Proof of Theorem jonairi
StepHypRef Expression
1 jonairi.0 . 2gonai ko'a bu'a ko'e gi ko'a bu'e ko'e
2 df-jonai 308 . 2go ko'a bu'a jonai bu'e ko'e gi gonai ko'a bu'a ko'e gi ko'a bu'e ko'e
31, 2bi-rev 102 1ko'a bu'a jonai bu'e ko'e
Colors of variables: sumti selbri bridi
Syntax hints:   gonai bgon 297   jonai sbjonai 307
This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 48  ax-ge-re 49  ax-ge-in 50
This theorem depends on definitions:  df-go 83  df-jonai 308
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator