Theorem casesifp

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	|- ( ph -> ( ps <-> ch ) )
	casesifp.2	|- ( -. ph -> ( ps <-> th ) )
Assertion	casesifp	|- ( ps <-> if- ( ph , ch , th ) )

Proof

Step	Hyp	Ref	Expression
1		casesifp.1	|- ( ph -> ( ps <-> ch ) )
2		casesifp.2	|- ( -. ph -> ( ps <-> th ) )
3	1 2	cases	|- ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )
4		df-ifp	|- ( if- ( ph , ch , th ) <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )
5	3 4	bitr4i	|- ( ps <-> if- ( ph , ch , th ) )