BiReplaceBi1Not0Ex1An1 Show Code edit
## Substitution
##
## (<-> ph (-. (E. x (/\ ps [ ch ] ] ] ))))
## (<-> [ ch ] [ th ] )
## (<-> ph (-. (E. x (/\ ps [ [ [ th ] ))))
##
thm (BiReplaceBi1Not0Ex1An1 () (
replacee (<-> ph (-. (E. x (/\ ps ch))))
substitution (<-> ch th))
(<-> ph (-. (E. x (/\ ps th))))
replacee
(<-> ph (-. (E. x (/\ ps ch))))
substitution
(<-> ch th)
ps anbi2i
(<-> (/\ ps ch) (/\ ps th))
x exbii
(<-> (E. x (/\ ps ch)) (E. x (/\ ps th)))
con4biir
(<-> (-. (E. x (/\ ps ch))) (-. (E. x (/\ ps th))))
ph bibi2i
(<-> (<-> ph (-. (E. x (/\ ps ch)))) (<-> ph (-. (E. x (/\ ps th)))))
mpbi
(<-> ph (-. (E. x (/\ ps th))))
)
edit