ZeqReplaceImp1Not0Zeq0 Show Code edit
## Substitution
##
## (-> ph (-. (z.= [ A ] ] ] C)))
## (z.= [ A ] [ B ] )
## (-> ph (-. (z.= [ [ [ B ] C)))
##
thm (ZeqReplaceImp1Not0Zeq0 () (
replacee (-> ph (-. (z.= A C)))
substitution (z.= A B))
(-> ph (-. (z.= B C)))
replacee substitution
(z.= A B)
C z.eqeq1i
(<-> (z.= A C) (z.= B C))
BiReplaceImp1Not0
(-> ph (-. (z.= B C)))
)
edit