Theorem brif2

Description: Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024)

	Ref	Expression
Assertion	brif2	$$⊢CRif\left(\phi ,A,B\right)\leftrightarrow if-\left(\phi ,CRA,CRB\right)$$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
2	1	breq2d	$$⊢\phi \to \left(CRif\left(\phi ,A,B\right)\leftrightarrow CRA\right)$$
3		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
4	3	breq2d	$$⊢\neg \phi \to \left(CRif\left(\phi ,A,B\right)\leftrightarrow CRB\right)$$
5	2 4	casesifp	$$⊢CRif\left(\phi ,A,B\right)\leftrightarrow if-\left(\phi ,CRA,CRB\right)$$