The implication fragment of Heyting's logic
is the minimal logical system for which deduction theorem
holds. This is known, but not emphasized enough.
In this note we present an elementary proof of this fact and propose
how to use it in order to promote the concept of many-valued logics in a
natural way, by giving a concept for the first lecture on this subject.