Inference Rules
Rules that say that if 1 or more well-formed formulas (wffs) that match the 1st part of the rule pattern are already part of the proof sequence, we can add to the proof sequence a new wff that matches the last part of the rule pattern.