Theorem ifeq12da

Description: Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021)

	Ref	Expression
Hypotheses	ifeq12da.1	|- ( ( ph /\ ps ) -> A = C )
	ifeq12da.2	|- ( ( ph /\ -. ps ) -> B = D )
Assertion	ifeq12da	|- ( ph -> if ( ps , A , B ) = if ( ps , C , D ) )

Proof

Step	Hyp	Ref	Expression
1		ifeq12da.1	|- ( ( ph /\ ps ) -> A = C )
2		ifeq12da.2	|- ( ( ph /\ -. ps ) -> B = D )
3	1	ifeq1da	|- ( ph -> if ( ps , A , B ) = if ( ps , C , B ) )
4		iftrue	|- ( ps -> if ( ps , C , B ) = C )
5		iftrue	|- ( ps -> if ( ps , C , D ) = C )
6	4 5	eqtr4d	|- ( ps -> if ( ps , C , B ) = if ( ps , C , D ) )
7	3 6	sylan9eq	|- ( ( ph /\ ps ) -> if ( ps , A , B ) = if ( ps , C , D ) )
8	2	ifeq2da	|- ( ph -> if ( ps , A , B ) = if ( ps , A , D ) )
9		iffalse	|- ( -. ps -> if ( ps , A , D ) = D )
10		iffalse	|- ( -. ps -> if ( ps , C , D ) = D )
11	9 10	eqtr4d	|- ( -. ps -> if ( ps , A , D ) = if ( ps , C , D ) )
12	8 11	sylan9eq	|- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = if ( ps , C , D ) )
13	7 12	pm2.61dan	|- ( ph -> if ( ps , A , B ) = if ( ps , C , D ) )