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

---

Theorem te-dual-r 366

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 360	. . . 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 81	. . 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 103	. . . . 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 79	. . . 4 ⊢ ganai ko'a te bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i
6		df-te 360	. . . . 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 81	. . . 4 ⊢ ganai ko'a bu'e ko'e ko'i gi ko'i te bu'e ko'e ko'a
8	5, 7	syl 20	. . 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 20	. 2 ⊢ ganai ko'i bu'a ko'e ko'a gi ko'i te bu'e ko'e ko'a
10		df-naja-t 103	. 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 80	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 98  te sbt 359

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  df-naja-t 103  df-te 360

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator