ZeqReplaceBi1Zeq1 Show Code edit
## Substitution
##
## (<-> ph (z.= A [ B ] ] ] ))
## (z.= [ B ] [ C ] )
## (<-> ph (z.= A [ [ [ C ] ))
##
thm (ZeqReplaceBi1Zeq1 () (
replacee (<-> ph (z.= A B))
substitution (z.= B C))
(<-> ph (z.= A C))
replacee substitution
(z.= B C)
A z.eqeq2i
(<-> (z.= A B) (z.= A C))
bitri
(<-> ph (z.= A C))
)
edit