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