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.
