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

---

Theorem te-dual-r 403

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 397	. . . 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 103	. . 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 125	. . . . 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 101	. . . 4 ⊢ ganai ko'a te bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i
6		df-te 397	. . . . 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 103	. . . 4 ⊢ ganai ko'a bu'e ko'e ko'i gi ko'i te bu'e ko'e ko'a
8	5, 7	syl 21	. . 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 21	. 2 ⊢ ganai ko'i bu'a ko'e ko'a gi ko'i te bu'e ko'e ko'a
10		df-naja-t 125	. 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 102	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 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