nic-idbl Show Code edit
# Double the terms. Since doubling is the same as negation,
# this can be viewed as a contraposition Inference. (Contributed
# by Jeff Hoffman, 17-Nov-2007.)
thm (nic-idbl () (nic-idbl.1 (-/\ ph (-/\ ps ps))) (-/\ (-/\ ps ps) (-/\ (-/\ ph ph) (-/\ ph ph))) nic-idbl.1 ps nic-imp nic-idbl.1 ph nic-imp nic-ich)
(-/\ (-/\ ps ps) (-/\ (-/\ ph ph) (-/\ ph ph)))
edit