 Soundness theorem for first-order logic

Every sentence derivable from a first-order theory is true in every model of that theory.

This is soundness of the first-order deduction system relative to its structure semantics.