Theorem 2if2

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

	Ref	Expression
Hypotheses	2if2.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 = 𝐴 )
	2if2.2	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ∧ 𝜃 ) → 𝐷 = 𝐵 )
	2if2.3	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜃 ) → 𝐷 = 𝐶 )
Assertion	2if2	⊢ ( 𝜑 → 𝐷 = if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2if2.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 = 𝐴 )
2		2if2.2	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ∧ 𝜃 ) → 𝐷 = 𝐵 )
3		2if2.3	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜃 ) → 𝐷 = 𝐶 )
4		iftrue	⊢ ( 𝜓 → if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) = 𝐴 )
5	4	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) = 𝐴 )
6	1 5	eqtr4d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 = if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) )
7	2	3expa	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∧ 𝜃 ) → 𝐷 = 𝐵 )
8		iftrue	⊢ ( 𝜃 → if ( 𝜃 , 𝐵 , 𝐶 ) = 𝐵 )
9	8	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∧ 𝜃 ) → if ( 𝜃 , 𝐵 , 𝐶 ) = 𝐵 )
10	7 9	eqtr4d	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∧ 𝜃 ) → 𝐷 = if ( 𝜃 , 𝐵 , 𝐶 ) )
11	3	3expa	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∧ ¬ 𝜃 ) → 𝐷 = 𝐶 )
12		iffalse	⊢ ( ¬ 𝜃 → if ( 𝜃 , 𝐵 , 𝐶 ) = 𝐶 )
13	12	eqcomd	⊢ ( ¬ 𝜃 → 𝐶 = if ( 𝜃 , 𝐵 , 𝐶 ) )
14	13	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∧ ¬ 𝜃 ) → 𝐶 = if ( 𝜃 , 𝐵 , 𝐶 ) )
15	11 14	eqtrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∧ ¬ 𝜃 ) → 𝐷 = if ( 𝜃 , 𝐵 , 𝐶 ) )
16	10 15	pm2.61dan	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝐷 = if ( 𝜃 , 𝐵 , 𝐶 ) )
17		iffalse	⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) = if ( 𝜃 , 𝐵 , 𝐶 ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) = if ( 𝜃 , 𝐵 , 𝐶 ) )
19	16 18	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝐷 = if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) )
20	6 19	pm2.61dan	⊢ ( 𝜑 → 𝐷 = if ( 𝜓 , 𝐴 , if ( 𝜃 , 𝐵 , 𝐶 ) ) )