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ψAifθBC

Proof

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