BiReplaceImp1Imp0 Show Code edit
## Substitution
##
## (-> ph (-> [ ps ] ] ] th))
## (<-> [ ps ] [ ch ] )
## (-> ph (-> [ [ [ ch ] th))
##
thm (BiReplaceImp1Imp0 () (
replacee (-> ph (-> ps th))
substitution (<-> ps ch))
(-> ph (-> ch th))
replacee substitution
(<-> ps ch)
th imbi1i
(<-> (-> ps th) (-> ch th))
sylib
(-> ph (-> ch th))
)
edit