Tautology (rule of inference)

In propositional logic, tautology is either of two commonly used rules of replacement.^[1][2][3] The rules are used to eliminate redundancy in disjunctions and conjunctions when they occur in logical proofs. They are:

The principle of idempotency of disjunction:

${\displaystyle P\lor P\Leftrightarrow P}$

and the principle of idempotency of conjunction:

${\displaystyle P\land P\Leftrightarrow P}$

Where "${\displaystyle \Leftrightarrow }$" is a metalogical symbol representing "can be replaced in a logical proof with."