P is a one-place predicate, t is a constant, v is a variable of P. P(t/v) denotes replacing v by t in P. In the proof of a theorem, it is given that Δ[itex]\vdash[/itex][itex]\forall[/itex]vP. (meaning [itex]\forall[/itex]vP is deduced from the set of statements Δ.) There exists an axiom scheme [itex]\vdash[/itex]\forall[/itex]vP[itex]\rightarrow[/itex](P(t/v). Then modus ponens is applied to these two to prove that Δ[itex]\vdash[/itex]P(t/v). I've never seen modus ponens applied to a deduction and it is used with so I scarcely know what to ask...how is this permissible? How does it work...same as regular modus ponens? Is there a proof that this is shows this is the same as modus ponens, or a definition that describes it?