disjunction and negation above. As with the rules for disjunction, these rules require that the variable quantified in one subformula does not appear free in the other subformula.

The rules for removing quantifiers from the antecedent are (note the change of quantifiers):
: is equivalent to ,
: is equivalent to .The rules for removing quantifiers from the consequent are:
: is equivalent to (under the assumption that ),
: is equivalent to .For example, when the range of quantification