ImpReplaceImp1Imp1 Show Code edit
## Substitution
##
## (-> ph (-> ps [ ch ] ] ] ))
## (-> [ ch ] [ th ] )
## (-> ph (-> ps [ [ [ th ] ))
##
thm (ImpReplaceImp1Imp1 () (
replacee (-> ph (-> ps ch))
substitution (-> ch th))
(-> ph (-> ps th))
replacee substitution
(-> ch th)
ps imim2i
(-> (-> ps ch) (-> ps th))
syl
(-> ph (-> ps th))
)
edit