Description: A theorem which could be used as sole axiom for the non-logical predicate
instead of ax-8 and ax-9 . Indeed, it is implied over propositional
calculus by the conjunction of ax-8 and ax-9 , as proved here. In the
other direction, one can prove ax-8 (respectively ax-9 ) from
bj-ax89 by using mpan2 (respectively mpan ) and equid . TODO:
move to main part. (Contributed by BJ, 3-Oct-2019)