First-Order Natural Deduction with Equality

An extension of the First-Order Natural Deduction Calculus to support the equality predicate of the First-Order Predicate Logic with Equality, called ${\mathcal{ND}}_{=}^1$. We add the following rules:

Where $C[A{]}_p$ is the formula $C$ which has a subterm $A$ at the position $p$. This basically means if $A=B$ we can replace all $A$s in $C$ with $B$s.

You can think of the postition $p$ as a position in a tree of $C$, which might look like this schematically:

In lots of ways equivalence behaves like equality in a logical way. Thats why we add the following additional rules for equivalence: