3anrot Show Code edit
# Rotation law for triple conjunction.
thm (3anrot () () (<-> (/\/\ ph ps ch) (/\/\ ps ch ph)) ph (/\ ps ch) ancom ph ps ch 3anass ps ch ph df-3an 3bitr4i)
(<-> (/\/\ ph ps ch) (/\/\ ps ch ph))
edit