Metamath Proof Explorer

Theorem elim2if

Description: Elimination of two conditional operators contained in a wff ch . (Contributed by Thierry Arnoux, 25-Jan-2017)

Ref Expression
Hypotheses elim2if.1 ⊢ if φ A if ψ B C = A → χ ↔ θ
elim2if.2 ⊢ if φ A if ψ B C = B → χ ↔ τ
elim2if.3 ⊢ if φ A if ψ B C = C → χ ↔ η
Assertion elim2if ⊢ χ ↔ φ ∧ θ ∨ ¬ φ ∧ ψ ∧ τ ∨ ¬ ψ ∧ η

Proof

Step Hyp Ref Expression
1 elim2if.1 ⊢ if φ A if ψ B C = A → χ ↔ θ
2 elim2if.2 ⊢ if φ A if ψ B C = B → χ ↔ τ
3 elim2if.3 ⊢ if φ A if ψ B C = C → χ ↔ η
4 iftrue ⊢ φ → if φ A if ψ B C = A
5 4 1 syl ⊢ φ → χ ↔ θ
6 iffalse ⊢ ¬ φ → if φ A if ψ B C = if ψ B C
7 6 eqeq1d ⊢ ¬ φ → if φ A if ψ B C = B ↔ if ψ B C = B
8 7 2 biimtrrdi ⊢ ¬ φ → if ψ B C = B → χ ↔ τ
9 6 eqeq1d ⊢ ¬ φ → if φ A if ψ B C = C ↔ if ψ B C = C
10 9 3 biimtrrdi ⊢ ¬ φ → if ψ B C = C → χ ↔ η
11 8 10 elimifd ⊢ ¬ φ → χ ↔ ψ ∧ τ ∨ ¬ ψ ∧ η
12 5 11 cases ⊢ χ ↔ φ ∧ θ ∨ ¬ φ ∧ ψ ∧ τ ∨ ¬ ψ ∧ η