anbi2 Show Code edit
####
# END METAMATH DUMP
####
thm (anbi2 () () (-> (<-> ph ps) (<-> (/\ ch ph) (/\ ch ps)))
(<-> ph ps) id
(-> (<-> ph ps) (<-> ph ps))
ch anbi2d
(-> (<-> ph ps) (<-> (/\ ch ph) (/\ ch ps)))
)
edit