biimp3ar Show Code edit
# Infer implication from a logical equivalence. Similar to [[biimpar]].
thm (biimp3ar () (biimp3a.1 (-> (/\ ph ps) (<-> ch th))) (-> (/\/\ ph ps th) ch) biimp3a.1 biimpar 3impa)
(-> (/\/\ ph ps th) ch)
edit