Type theory, meaning systems in textbooks and theorem provers such as the HOL family based on Church's type theory, are supersets of first order logic. Modus ponens is usually a derived rule of inference, but is perfectly valid, as are other first order theorems and rules of inference.
Type theory though takes a different approach than set theory though, especially compared with ZFC. ZFC has only sets, and all variables range over sets, where in type theory variables, constants, and terms generally have types. Expressions are not syntactically valid unless function and argument types match up properly.
So a proof in type theory need not look any different than a proof in first order logic, though technically there should be type annotations at least on enough variables to determine the types of the terms in it.