nic-luk2 Show Code edit
# Proof of [[luk-2]] from [[nic-ax]] and [[nic-mp]]. (Contributed by Jeff
# Hoffman, 18-Nov-2007.)
thm (nic-luk2 () () (-> (-> (-. ph) ph) ph) (-. ph) ph nic-dfim nic-bi2 ph nic-dfneg (-/\ ph ph) nic-id nic-iimp1 nic-isw2 nic-iimp1 nic-isw1 (-> (-. ph) ph) ph nic-dfim nic-bi1 nic-mp)
(-> (-> (-. ph) ph) ph)
edit