Theorem 2if2

Description: Resolve two nested conditionals. (Contributed by Alexander van der Vekens, 27-Mar-2018)

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

Proof

Step	Hyp	Ref	Expression
1		2if2.1	|- ( ( ph /\ ps ) -> D = A )
2		2if2.2	|- ( ( ph /\ -. ps /\ th ) -> D = B )
3		2if2.3	|- ( ( ph /\ -. ps /\ -. th ) -> D = C )
4		iftrue	|- ( ps -> if ( ps , A , if ( th , B , C ) ) = A )
5	4	adantl	|- ( ( ph /\ ps ) -> if ( ps , A , if ( th , B , C ) ) = A )
6	1 5	eqtr4d	|- ( ( ph /\ ps ) -> D = if ( ps , A , if ( th , B , C ) ) )
7	2	3expa	|- ( ( ( ph /\ -. ps ) /\ th ) -> D = B )
8		iftrue	|- ( th -> if ( th , B , C ) = B )
9	8	adantl	|- ( ( ( ph /\ -. ps ) /\ th ) -> if ( th , B , C ) = B )
10	7 9	eqtr4d	|- ( ( ( ph /\ -. ps ) /\ th ) -> D = if ( th , B , C ) )
11	3	3expa	|- ( ( ( ph /\ -. ps ) /\ -. th ) -> D = C )
12		iffalse	|- ( -. th -> if ( th , B , C ) = C )
13	12	eqcomd	|- ( -. th -> C = if ( th , B , C ) )
14	13	adantl	|- ( ( ( ph /\ -. ps ) /\ -. th ) -> C = if ( th , B , C ) )
15	11 14	eqtrd	|- ( ( ( ph /\ -. ps ) /\ -. th ) -> D = if ( th , B , C ) )
16	10 15	pm2.61dan	|- ( ( ph /\ -. ps ) -> D = if ( th , B , C ) )
17		iffalse	|- ( -. ps -> if ( ps , A , if ( th , B , C ) ) = if ( th , B , C ) )
18	17	adantl	|- ( ( ph /\ -. ps ) -> if ( ps , A , if ( th , B , C ) ) = if ( th , B , C ) )
19	16 18	eqtr4d	|- ( ( ph /\ -. ps ) -> D = if ( ps , A , if ( th , B , C ) ) )
20	6 19	pm2.61dan	|- ( ph -> D = if ( ps , A , if ( th , B , C ) ) )