nic-ich Show Code edit
# Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.)
thm (nic-ich () (nic-ich.1 (-/\ ph (-/\ ps ps)) nic-ich.2 (-/\ ps (-/\ ch ch))) (-/\ ph (-/\ ch ch)) nic-ich.2 nic-isw1 nic-ich.1 (-/\ ch ch) nic-imp nic-mp)
(-/\ ph (-/\ ch ch))
edit