EqReplaceNot0Eq1 Show Code edit
## Substitution
##
## (-. (= A [ B ] ] ] ))
## (= [ B ] [ C ] )
## (-. (= A [ [ [ C ] ))
##
thm (EqReplaceNot0Eq1 () (
replacee (-. (= A B))
substitution (= B C))
(-. (= A C))
replacee
(-. (= A B))
substitution
(= B C)
A eqeq2i
(<-> (= A B) (= A C))
con4biir
(<-> (-. (= A B)) (-. (= A C)))
mpbi
(-. (= A C))
)
edit