nic-luk3 Show Code edit
# Proof of [[luk-3]] from [[nic-ax]] and [[nic-mp]]. (Contributed by Jeff
# Hoffman, 18-Nov-2007.)
thm (nic-luk3 () () (-> ph (-> (-. ph) ps)) (-. ph) ps nic-dfim nic-bi1 ph nic-dfneg nic-bi2 ph nic-id nic-iimp1 nic-iimp2 ph (-> (-. ph) ps) nic-dfim nic-bi1 nic-mp)
(-> ph (-> (-. ph) ps))
edit