dedlemb Show Code edit
## Weak Deduction Theorem Lemma
thm (dedlemb () () (-> (-. ph) (<-> ch (\/ (/\ ps ph) (/\ ch (-. ph))))) (/\ ch (-. ph)) (/\ ps ph) olc expcom ph (-> ps ch) pm2.21 com23 imp3a ch (-. ph) pm3.26 (-. ph) a1i jaod impbid)
(-> (-. ph) (<-> ch (\/ (/\ ps ph) (/\ ch (-. ph)))))
edit