Metamath Proof Explorer

Theorem elim2ifim

Description: Elimination of two conditional operators for an implication. (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 → χ ↔ η
elim2ifim.1 ⊢ φ → θ
elim2ifim.2 ⊢ ¬ φ ∧ ψ → τ
elim2ifim.3 ⊢ ¬ φ ∧ ¬ ψ → η
Assertion elim2ifim ⊢ χ

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 elim2ifim.1 ⊢ φ → θ
5 elim2ifim.2 ⊢ ¬ φ ∧ ψ → τ
6 elim2ifim.3 ⊢ ¬ φ ∧ ¬ ψ → η
7 exmid ⊢ φ ∨ ¬ φ
8 4 ancli ⊢ φ → φ ∧ θ
9 pm4.42 ⊢ ¬ φ ↔ ¬ φ ∧ ψ ∨ ¬ φ ∧ ¬ ψ
10 5 ex ⊢ ¬ φ → ψ → τ
11 10 ancld ⊢ ¬ φ → ψ → ψ ∧ τ
12 11 imp ⊢ ¬ φ ∧ ψ → ψ ∧ τ
13 6 ex ⊢ ¬ φ → ¬ ψ → η
14 13 ancld ⊢ ¬ φ → ¬ ψ → ¬ ψ ∧ η
15 14 imp ⊢ ¬ φ ∧ ¬ ψ → ¬ ψ ∧ η
16 12 15 orim12i ⊢ ¬ φ ∧ ψ ∨ ¬ φ ∧ ¬ ψ → ψ ∧ τ ∨ ¬ ψ ∧ η
17 9 16 sylbi ⊢ ¬ φ → ψ ∧ τ ∨ ¬ ψ ∧ η
18 17 ancli ⊢ ¬ φ → ¬ φ ∧ ψ ∧ τ ∨ ¬ ψ ∧ η
19 8 18 orim12i ⊢ φ ∨ ¬ φ → φ ∧ θ ∨ ¬ φ ∧ ψ ∧ τ ∨ ¬ ψ ∧ η
20 7 19 ax-mp ⊢ φ ∧ θ ∨ ¬ φ ∧ ψ ∧ τ ∨ ¬ ψ ∧ η
21 1 2 3 elim2if ⊢ χ ↔ φ ∧ θ ∨ ¬ φ ∧ ψ ∧ τ ∨ ¬ ψ ∧ η
22 20 21 mpbir ⊢ χ