nic-axALT Show Code edit
# A direct proof of [[nic-ax]].
thm (nic-axALT () () (-/\ (-/\ ph (-/\ ch ps)) (-/\ (-/\ ta (-/\ ta ta)) (-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th))))) ch ps pm3.26 ph imim2i ph ch con3 th imim2d syl ta anidm biimpri jctil ch ps df-nand ph anbi2i notbii ph (-/\ ch ps) df-nand ph (/\ ch ps) iman 3bitr4i (-/\ ta (-/\ ta ta)) (-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th))) df-nand ta ta df-nand ta anbi2i notbii ta (-/\ ta ta) df-nand ta (/\ ta ta) iman 3bitr4i th ch df-nand th ch imnan bitr4i (-/\ ph th) (-/\ ph th) df-nand (-/\ ph th) anidm ph th df-nand ph th imnan ph th con2b bitr3i 3bitri notbii bitri anbi12i notbii (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th)) df-nand (-> th (-. ch)) (-> th (-. ph)) iman 3bitr4i anbi12i notbii bitri anbi12i notbii (-> ph (/\ ch ps)) (/\ (-> ta (/\ ta ta)) (-> (-> th (-. ch)) (-> th (-. ph)))) iman bitr4i mpbir (-/\ ph (-/\ ch ps)) (-/\ (-/\ ta (-/\ ta ta)) (-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th)))) df-nand mpbir)
(-/\ (-/\ ph (-/\ ch ps)) (-/\ (-/\ ta (-/\ ta ta)) (-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th)))))
edit