nic-imp Show Code edit
# Inference for [[nic-mp]] using [[nic-ax]] as major premise. (Contributed
# by Jeff Hoffman, 17-Nov-2007.)
thm (nic-imp () (nic-imp.1 (-/\ ph (-/\ ch ps))) (-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th))) nic-imp.1 ph ch ps ta th nic-ax nic-mp)
(-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th)))
edit