EqReplaceImp1Eq1Add1 Show Code edit
## Substitution
##
## (-> ph (= A (+ B [ C ] ] ] )))
## (= [ C ] [ D ] )
## (-> ph (= A (+ B [ [ [ D ] )))
##
thm (EqReplaceImp1Eq1Add1 () (
replacee (-> ph (= A (+ B C)))
substitution (= C D))
(-> ph (= A (+ B D)))
replacee substitution
(= C D)
B addeq2i
(= (+ B C) (+ B D))
EqReplaceImp1Eq1
(-> ph (= A (+ B D)))
)
edit