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	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
	casesifp.2	$$⊢\neg \phi \to \left(\psi \leftrightarrow \theta \right)$$
Assertion	casesifp	$$⊢\psi \leftrightarrow if-\left(\phi ,\chi ,\theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		casesifp.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2		casesifp.2	$$⊢\neg \phi \to \left(\psi \leftrightarrow \theta \right)$$
3	1 2	cases	$$⊢\psi \leftrightarrow \left(\left(\phi \wedge \chi \right)\vee \left(\neg \phi \wedge \theta \right)\right)$$
4		df-ifp	$$⊢if-\left(\phi ,\chi ,\theta \right)\leftrightarrow \left(\left(\phi \wedge \chi \right)\vee \left(\neg \phi \wedge \theta \right)\right)$$
5	3 4	bitr4i	$$⊢\psi \leftrightarrow if-\left(\phi ,\chi ,\theta \right)$$