ZeqReplaceBi1An1Not0Zeq0 Show Code edit
## Substitution
##
## (<-> ph (/\ ps (-. (z.= [ A ] ] ] C))))
## (z.= [ A ] [ B ] )
## (<-> ph (/\ ps (-. (z.= [ [ [ B ] C))))
##
thm (ZeqReplaceBi1An1Not0Zeq0 () (
replacee (<-> ph (/\ ps (-. (z.= A C))))
substitution (z.= A B))
(<-> ph (/\ ps (-. (z.= B C))))
replacee substitution
(z.= A B)
C z.eqeq1i
(<-> (z.= A C) (z.= B C))
BiReplaceBi1An1Not0
(<-> ph (/\ ps (-. (z.= B C))))
)
edit