An axiom schema is valid if and only if every instance of the schema is valid. The schema above is valid, as are the schemas shown below.
Reflexivity  φ ⇒ φ 
Negation Elimination  ¬¬φ ⇒ φ 
Negation Introduction  φ ⇒ ¬¬φ 
Tautology  φ ∨ ¬φ 
In what follows, we use both nonvalid and valid axiom schemas. Nonvalid schemas play a role in defining rules of inference, and valid schemas are used as components of deductive proof systems.
