impexp Show Code edit
# Import-export theorem. Part of Theorem *4.87 of [bib/WhiteheadRussell]
# p. 122.
## Import-Export Theorem
## left('Equivalence', 'โˆงโ†’') right('Equivalence', 'โ†’โ†’')
thm (impexp () () (<-> (-> (/\ ph ps) ch) (-> ph (-> ps ch))) ph ps df-an ch imbi1i ph ps ch expt ph ps ch impt impbii bitri)
(<-> (-> (/\ ph ps) ch) (-> ph (-> ps ch)))
edit