---

Step * of Lemma hp-angle-sum-subst

∀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
   THEN (Unfold `hp-angle-sum` 0 THEN Unfold `hp-angle-sum` -2)
   THEN (ExRepD THEN InstConcl [⌜p⌝;⌜p'⌝;⌜d'⌝;⌜f'⌝]⋅ THEN Auto)
   THEN InstLemma `geo-cong-angle-transitivity` [⌜g⌝;⌜i⌝;⌜j⌝;⌜k⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜y⌝;⌜p⌝]⋅
   THEN EAuto 1) }

---

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
  THEN  (Unfold  `hp-angle-sum`  0  THEN  Unfold  `hp-angle-sum`  -2)
  THEN  (ExRepD  THEN  InstConcl  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index