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