Theorem brif12

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

	Ref	Expression
Assertion	brif12	$$⊢if\left(\phi ,A,B\right)Rif\left(\phi ,C,D\right)\leftrightarrow if-\left(\phi ,ARC,BRD\right)$$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
2		iftrue	$$⊢\phi \to if\left(\phi ,C,D\right)=C$$
3	1 2	breq12d	$$⊢\phi \to \left(if\left(\phi ,A,B\right)Rif\left(\phi ,C,D\right)\leftrightarrow ARC\right)$$
4		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
5		iffalse	$$⊢\neg \phi \to if\left(\phi ,C,D\right)=D$$
6	4 5	breq12d	$$⊢\neg \phi \to \left(if\left(\phi ,A,B\right)Rif\left(\phi ,C,D\right)\leftrightarrow BRD\right)$$
7	3 6	casesifp	$$⊢if\left(\phi ,A,B\right)Rif\left(\phi ,C,D\right)\leftrightarrow if-\left(\phi ,ARC,BRD\right)$$