Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  te-dual

Theorem te-dual 401
Description: Self-duality property for {te}. (Contributed by la korvo, 13-Aug-2024.)
Hypothesis
Ref Expression
te-dual.0ko'a bu'a naja bu'e ko'e ko'i
Assertion
Ref Expression
te-dualko'i te bu'a naja te bu'e ko'e ko'a
Distinct variable group:   bu'a , bu'e

Proof of Theorem te-dual
StepHypRef Expression
1 df-te 397 . . . 4go ko'i te bu'a ko'e ko'a gi ko'a bu'a ko'e ko'i
21go-ganai 85 . . 3ganai ko'i te bu'a ko'e ko'a gi ko'a bu'a ko'e ko'i
3 te-dual.0 . . . . 5ko'a bu'a naja bu'e ko'e ko'i
4 df-naja-t 125 . . . . 5go ko'a bu'a naja bu'e ko'e ko'i gi ganai ko'a bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i
53, 4bi 101 . . . 4ganai ko'a bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i
6 df-te 397 . . . . 5go ko'i te bu'e ko'e ko'a gi ko'a bu'e ko'e ko'i
76bi-rev-syl 103 . . . 4ganai ko'a bu'e ko'e ko'i gi ko'i te bu'e ko'e ko'a
85, 7syl 21 . . 3ganai ko'a bu'a ko'e ko'i gi ko'i te bu'e ko'e ko'a
92, 8syl 21 . 2ganai ko'i te bu'a ko'e ko'a gi ko'i te bu'e ko'e ko'a
10 df-naja-t 125 . 2go ko'i te bu'a naja te bu'e ko'e ko'a gi ganai ko'i te bu'a ko'e ko'a gi ko'i te bu'e ko'e ko'a
119, 10bi-rev 102 1ko'i te bu'a naja te bu'e ko'e ko'a
Colors of variables: sumti selbri bridi
Syntax hints:   ganai bgan 9   naja sbnaja 120   te sbt 396
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-naja-t 125  df-te 397
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator