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 ⊢ φ ∧ ψ → D = A
2if2.2 ⊢ φ ∧ ¬ ψ ∧ θ → D = B
2if2.3 ⊢ φ ∧ ¬ ψ ∧ ¬ θ → D = C
Assertion 2if2 ⊢ φ → D = if ψ A if θ B C

Proof

Step Hyp Ref Expression
1 2if2.1 ⊢ φ ∧ ψ → D = A
2 2if2.2 ⊢ φ ∧ ¬ ψ ∧ θ → D = B
3 2if2.3 ⊢ φ ∧ ¬ ψ ∧ ¬ θ → D = C
4 iftrue ⊢ ψ → if ψ A if θ B C = A
5 4 adantl ⊢ φ ∧ ψ → if ψ A if θ B C = A
6 1 5 eqtr4d ⊢ φ ∧ ψ → D = if ψ A if θ B C
7 2 3expa ⊢ φ ∧ ¬ ψ ∧ θ → D = B
8 iftrue ⊢ θ → if θ B C = B
9 8 adantl ⊢ φ ∧ ¬ ψ ∧ θ → if θ B C = B
10 7 9 eqtr4d ⊢ φ ∧ ¬ ψ ∧ θ → D = if θ B C
11 3 3expa ⊢ φ ∧ ¬ ψ ∧ ¬ θ → D = C
12 iffalse ⊢ ¬ θ → if θ B C = C
13 12 eqcomd ⊢ ¬ θ → C = if θ B C
14 13 adantl ⊢ φ ∧ ¬ ψ ∧ ¬ θ → C = if θ B C
15 11 14 eqtrd ⊢ φ ∧ ¬ ψ ∧ ¬ θ → D = if θ B C
16 10 15 pm2.61dan ⊢ φ ∧ ¬ ψ → D = if θ B C
17 iffalse ⊢ ¬ ψ → if ψ A if θ B C = if θ B C
18 17 adantl ⊢ φ ∧ ¬ ψ → if ψ A if θ B C = if θ B C
19 16 18 eqtr4d ⊢ φ ∧ ¬ ψ → D = if ψ A if θ B C
20 6 19 pm2.61dan ⊢ φ → D = if ψ A if θ B C