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

---

Theorem subt 463

Description: Theorems are invariant under substitution. (Contributed by la korvo, 9-Jul-2025.)

Hypothesis

Ref	Expression
subt.0	⊢ broda

Assertion

Ref	Expression
subt	⊢ [ ko'a / da ] broda

---

Proof of Theorem subt

Step	Hyp	Ref	Expression
1		subt.0	. 2 ⊢ broda
2	1	nfth 443	. . 3 ⊢ na'a'u da zo'u broda
3	2	subf 462	. 2 ⊢ go [ ko'a / da ] broda gi broda
4	1, 3	bi-rev 102	1 ⊢ [ ko'a / da ] broda

Colors of variables: sumti selbri bridi

Syntax hints:   [ bsub 448

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  ax-gen1 224  ax-spec1 228  ax-qi1 234  ax-ro1-nf 249  ax-ex 418  ax-eb 420  ax-eq 422

This theorem depends on definitions:  df-go 83  df-nahahu 437  df-sub 449

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator