Idempotency of entailment is a property of logical systems that states that one may derive the same consequences from many instances of a hypothesis as from just one. In sequent calculi this property can be captured by a structural rule

Structural rule

In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgements or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic...

 called contraction and in such systems one may say that entailment

Entailment

In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...

 is idempotent just in case contraction is an admissible rule

Admissible rule

In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense,...

.

Rule of Contraction: from

A,C,C -> B

is derived

A,C -> B.

Or in sequent calculus

Sequent calculus

In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...

notation,