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	|- ( ph -> ( ps <-> ch ) )
	ifbieq12d2.2	|- ( ( ph /\ ps ) -> A = C )
	ifbieq12d2.3	|- ( ( ph /\ -. ps ) -> B = D )
Assertion	ifbieq12d2	|- ( ph -> if ( ps , A , B ) = if ( ch , C , D ) )

Proof

Step	Hyp	Ref	Expression
1		ifbieq12d2.1	|- ( ph -> ( ps <-> ch ) )
2		ifbieq12d2.2	|- ( ( ph /\ ps ) -> A = C )
3		ifbieq12d2.3	|- ( ( ph /\ -. ps ) -> B = D )
4	2 3	ifeq12da	|- ( ph -> if ( ps , A , B ) = if ( ps , C , D ) )
5	1	ifbid	|- ( ph -> if ( ps , C , D ) = if ( ch , C , D ) )
6	4 5	eqtrd	|- ( ph -> if ( ps , A , B ) = if ( ch , C , D ) )