Theorem brif1

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

	Ref	Expression
Assertion	brif1	$$⊢if\left(\phi ,A,B\right)RC\leftrightarrow if-\left(\phi ,ARC,BRC\right)$$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
2	1	breq1d	$$⊢\phi \to \left(if\left(\phi ,A,B\right)RC\leftrightarrow ARC\right)$$
3		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
4	3	breq1d	$$⊢\neg \phi \to \left(if\left(\phi ,A,B\right)RC\leftrightarrow BRC\right)$$
5	2 4	casesifp	$$⊢if\left(\phi ,A,B\right)RC\leftrightarrow if-\left(\phi ,ARC,BRC\right)$$