elimh Show Code edit
# Hypothesis builder for weak deduction theorem. For more information,
# see the Deduction Theorem link on the Metamath Proof Explorer home
# page.
## Hypothesis builder for weak deduction theorem
thm (elimh () (elimh.1 (-> (<-> ph (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> ch ta)) elimh.2 (-> (<-> ps (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> th ta)) elimh.3 th) ta ch ph ps dedlema elimh.1 syl ibi elimh.3 ch ps ph dedlemb elimh.2 syl mpbii pm2.61i)
ta
edit