Every axiom, definition, and theorem in Metamath is actually a template where no matter what you plug in for the free variables, you get a statement that's considered true in the system. So, for example:
Q → (P → Q)
Allows you to write sentences like
(A = 0) → ((∀ x ∈ R (0 < x → A < x)) → (A = 0))
This is kind of like a Scheme macro, but a really surprising thing about Metamath is that the sort of substitution it employs is not hygienic. If you happen to be using a local variable x, and you plug in a formula that has x free, the formula will “capture” the x in its new context.
In Scheme, if you plug a bit of code into another bit of code this way, and both bits of code are using a variable named x, Scheme behaves as though it's silently renaming one of the variables so the two don't conflict... unless the two x's actually refer to the same global variable or something—you can see it gets rather complicated. Lisp doesn't bother. It just plugs in the code. If variables get crossed, they get crossed.
Apparently doing it the Lisp way makes the Metamath proof-checker a lot simpler. Interesting.