The rule
 |
where 
means "implies," which is the sole rule of inference in propositional calculus. This rule states that if each of 
and 
is either an axiom or a theorem formally deduced from axioms by application of inference rules, then 
is also a formal theorem.
