Theorem ifeq3da

Description: Given an expression C containing if ( ps , E , F ) , substitute (hypotheses .1 and .2) and evaluate (hypotheses .3 and .4) it for both cases at the same time. (Contributed by Thierry Arnoux, 13-Dec-2021)

	Ref	Expression
Hypotheses	ifeq3da.1	|- ( if ( ps , E , F ) = E -> C = G )
	ifeq3da.2	|- ( if ( ps , E , F ) = F -> C = H )
	ifeq3da.3	|- ( ph -> G = A )
	ifeq3da.4	|- ( ph -> H = B )
Assertion	ifeq3da	|- ( ph -> if ( ps , A , B ) = C )

Proof

Step	Hyp	Ref	Expression
1		ifeq3da.1	|- ( if ( ps , E , F ) = E -> C = G )
2		ifeq3da.2	|- ( if ( ps , E , F ) = F -> C = H )
3		ifeq3da.3	|- ( ph -> G = A )
4		ifeq3da.4	|- ( ph -> H = B )
5		iftrue	|- ( ps -> if ( ps , E , F ) = E )
6	5 1	syl	|- ( ps -> C = G )
7	6	adantl	|- ( ( ph /\ ps ) -> C = G )
8	3	adantr	|- ( ( ph /\ ps ) -> G = A )
9	7 8	eqtr2d	|- ( ( ph /\ ps ) -> A = C )
10		iffalse	|- ( -. ps -> if ( ps , E , F ) = F )
11	10 2	syl	|- ( -. ps -> C = H )
12	11	adantl	|- ( ( ph /\ -. ps ) -> C = H )
13	4	adantr	|- ( ( ph /\ -. ps ) -> H = B )
14	12 13	eqtr2d	|- ( ( ph /\ -. ps ) -> B = C )
15	9 14	ifeqda	|- ( ph -> if ( ps , A , B ) = C )