This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝜃 , 𝐵 , 𝐶 ) ) )