Theorem ifeqda

Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		ifeqda.1	|- ( ( ph /\ ps ) -> A = C )
2		ifeqda.2	|- ( ( ph /\ -. ps ) -> B = C )
3		iftrue	|- ( ps -> if ( ps , A , B ) = A )
4	3	adantl	|- ( ( ph /\ ps ) -> if ( ps , A , B ) = A )
5	4 1	eqtrd	|- ( ( ph /\ ps ) -> if ( ps , A , B ) = C )
6		iffalse	|- ( -. ps -> if ( ps , A , B ) = B )
7	6	adantl	|- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = B )
8	7 2	eqtrd	|- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = C )
9	5 8	pm2.61dan	|- ( ph -> if ( ps , A , B ) = C )