Theorem ifbieq12d2

Description: Equivalence deduction for conditional operators. (Contributed by Thierry Arnoux, 14-Feb-2017) (Proof shortened by Wolf Lammen, 24-Jun-2021)

	Ref	Expression
Hypotheses	ifbieq12d2.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
	ifbieq12d2.2	$$⊢\left(\phi \wedge \psi \right)\to A=C$$
	ifbieq12d2.3	$$⊢\left(\phi \wedge \neg \psi \right)\to B=D$$
Assertion	ifbieq12d2	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifbieq12d2.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2		ifbieq12d2.2	$$⊢\left(\phi \wedge \psi \right)\to A=C$$
3		ifbieq12d2.3	$$⊢\left(\phi \wedge \neg \psi \right)\to B=D$$
4	2 3	ifeq12da	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\psi ,C,D\right)$$
5	1	ifbid	$$⊢\phi \to if\left(\psi ,C,D\right)=if\left(\chi ,C,D\right)$$
6	4 5	eqtrd	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)$$