Description: The case in which ph is denied, ps is affirmed, and ph is
affirmed is excluded. This is evident since ph cannot at the same
time be denied and affirmed. Axiom 1 of Frege1879 p. 26. Identical to
ax-1 . (Contributed by RP, 24-Dec-2019)(New usage is discouraged.)