Description: Version of cases expressed using if- . Case disjunction according
to the value of ph . One can see this as a proof that the two
hypotheses characterize the conditional operator for propositions. For
the converses, see ifptru and ifpfal . (Contributed by BJ, 20-Sep-2019)