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

---

Theorem te-dual-r 329

Description: Shift {te} to the right of an implication. (Contributed by la korvo, 13-Aug-2024.)

Hypothesis

Ref	Expression
te-dual-r.0	⊢ ko'a te bu'a naja bu'e ko'e ko'i

Assertion

Ref	Expression
te-dual-r	⊢ ko'i bu'a naja te bu'e ko'e ko'a

Distinct variable group:   bu'a ,bu'e

---

Proof of Theorem te-dual-r

Step	Hyp	Ref	Expression
1		df-te 323	. . . 4 ⊢ go ko'a te bu'a ko'e ko'i gi ko'i bu'a ko'e ko'a
2	1	bi-rev-syl 71	. . 3 ⊢ ganai ko'i bu'a ko'e ko'a gi ko'a te bu'a ko'e ko'i
3		te-dual-r.0	. . . . 5 ⊢ ko'a te bu'a naja bu'e ko'e ko'i
4		df-naja-t 93	. . . . 5 ⊢ go ko'a te bu'a naja bu'e ko'e ko'i gi ganai ko'a te bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i
5	3, 4	bi 69	. . . 4 ⊢ ganai ko'a te bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i
6		df-te 323	. . . . 5 ⊢ go ko'i te bu'e ko'e ko'a gi ko'a bu'e ko'e ko'i
7	6	bi-rev-syl 71	. . . 4 ⊢ ganai ko'a bu'e ko'e ko'i gi ko'i te bu'e ko'e ko'a
8	5, 7	syl 18	. . 3 ⊢ ganai ko'a te bu'a ko'e ko'i gi ko'i te bu'e ko'e ko'a
9	2, 8	syl 18	. 2 ⊢ ganai ko'i bu'a ko'e ko'a gi ko'i te bu'e ko'e ko'a
10		df-naja-t 93	. 2 ⊢ go ko'i bu'a naja te bu'e ko'e ko'a gi ganai ko'i bu'a ko'e ko'a gi ko'i te bu'e ko'e ko'a
11	9, 10	bi-rev 70	1 ⊢ ko'i bu'a naja te bu'e ko'e ko'a

Colors of variables: sumti selbri bridi

Syntax hints:  ganai bgan 9  naja sbnaja 88  te sbt 322

This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 14  ax-ge-le 34  ax-ge-re 35  ax-ge-in 36

This theorem depends on definitions:  df-go 52  df-naja-t 93  df-te 323

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator