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.
" is a metalogical symbol representing "can be replaced in a logical proof with".
is the conclusion of a valid proof,[4] while the equivalent semantic consequence
" appears on a line of a proof, it can be replaced with "
"; or as the statement of a truth-functional tautology or theorem of propositional logic.
The principle was stated as a theorem of propositional logic by Russell and Whitehead in Principia Mathematica as: and where