Theorems are those logical formulas ${\displaystyle \phi }$  where ${\displaystyle \vdash \phi }$  is the conclusion of a valid proof,^[4] while the equivalent semantic consequence ${\displaystyle \models \phi }$  indicates a tautology.

The tautology rule may be expressed as a sequent:

${\displaystyle P\lor P\vdash P}$ 

and

${\displaystyle P\land P\vdash P}$ 

where ${\displaystyle \vdash }$  is a metalogical symbol meaning that ${\displaystyle P}$  is a syntactic consequence of ${\displaystyle P\lor P}$ , in the one case, ${\displaystyle P\land P}$  in the other, in some logical system;

or as a rule of inference:

${\displaystyle {\frac {P\lor P}{\therefore P}}}$ 

and

${\displaystyle {\frac {P\land P}{\therefore P}}}$ 

where the rule is that wherever an instance of "${\displaystyle P\lor P}$ " or "${\displaystyle P\land P}$ " appears on a line of a proof, it can be replaced with "${\displaystyle P}$ ";

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:

${\displaystyle (P\lor P)\to P}$ 

and

${\displaystyle (P\land P)\to P}$ 

where ${\displaystyle P}$  is a proposition expressed in some formal system.