nic-isw2 Show Code edit
# Inference for swapping nested terms. (Contributed by Jeff Hoffman,
# 17-Nov-2007.)
thm (nic-isw2 () (nic-isw2.1 (-/\ ps (-/\ th ph))) (-/\ ps (-/\ ph th)) nic-isw2.1 ph th nic-swap ps nic-imp nic-mp nic-isw1)
(-/\ ps (-/\ ph th))
edit