nic-idel Show Code edit
# Inference to remove the trailing term. (Contributed by Jeff Hoffman,
# 17-Nov-2007.)
thm (nic-idel () (nic-idel.1 (-/\ ph (-/\ ch ps))) (-/\ ph (-/\ ch ch)) ch nic-id nic-isw1 nic-idel.1 (-/\ ch ch) nic-imp nic-mp)
(-/\ ph (-/\ ch ch))
edit