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