Subjunction introduction. It reflects the deduction theorem, but is an inference rule, not a metatheorem.