Even though it is not ordinarily part of propositional calculus, the equality predicate is introduced here so that the soundness of definition df-tru can be checked by the same algorithm as is used for predicate calculus. Its first real use is in Theorem weq in the predicate calculus section below. For those who want propositional calculus to be self-contained, i.e., to use wff variables only, the alternate definition dftru2 may be adopted and this subsection moved down to just above weq below. However, the use of dftru2 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid.