---

Step * of Lemma hp-angle-sum-subst2

∀g:EuclideanPlane. ∀a,b,c,d,e,f,x,y,z,i,j,k:Point.  (abc + def ≅ xyz ⇒ abc ≅a ijk ⇒ ijk + def ≅ xyz)
BY
{ Auto }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. abc + def ≅ xyz
15. abc ≅a ijk
⊢ ijk + def ≅ xyz

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f,x,y,z,i,j,k:Point.
    (abc  +  def  \mcong{}  xyz  {}\mRightarrow{}  abc  \mcong{}\msuba{}  ijk  {}\mRightarrow{}  ijk  +  def  \mcong{}  xyz)


By

---

Latex:
Auto

---

Home Index