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)
Ref | Expression | ||
---|---|---|---|
Hypotheses | casesifp.1 | |
|
casesifp.2 | |
||
Assertion | casesifp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | casesifp.1 | |
|
2 | casesifp.2 | |
|
3 | 1 2 | cases | |
4 | df-ifp | |
|
5 | 3 4 | bitr4i | |