dedlema Show Code edit
## Weak Deduction Theorem Lemma
thm (dedlema () () (-> ph (<-> ps (\/ (/\ ps ph) (/\ ch (-. ph))))) ps (/\ ch (-. ph)) orc ph ps idd ph ps pm2.24 ch adantld jaod impbid2 ph ps iba (/\ ch (-. ph)) orbi1d bitrd)
(-> ph (<-> ps (\/ (/\ ps ph) (/\ ch (-. ph)))))
edit