Metamath Proof Explorer

Theorem elimifd

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

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

Proof

Step Hyp Ref Expression
1 elimifd.1 ⊢ φ → if ψ A B = A → χ ↔ θ
2 elimifd.2 ⊢ φ → if ψ A B = B → χ ↔ τ
3 exmid ⊢ ψ ∨ ¬ ψ
4 3 biantrur ⊢ χ ↔ ψ ∨ ¬ ψ ∧ χ
5 4 a1i ⊢ φ → χ ↔ ψ ∨ ¬ ψ ∧ χ
6 andir ⊢ ψ ∨ ¬ ψ ∧ χ ↔ ψ ∧ χ ∨ ¬ ψ ∧ χ
7 6 a1i ⊢ φ → ψ ∨ ¬ ψ ∧ χ ↔ ψ ∧ χ ∨ ¬ ψ ∧ χ
8 iftrue ⊢ ψ → if ψ A B = A
9 8 1 syl5 ⊢ φ → ψ → χ ↔ θ
10 9 pm5.32d ⊢ φ → ψ ∧ χ ↔ ψ ∧ θ
11 iffalse ⊢ ¬ ψ → if ψ A B = B
12 11 2 syl5 ⊢ φ → ¬ ψ → χ ↔ τ
13 12 pm5.32d ⊢ φ → ¬ ψ ∧ χ ↔ ¬ ψ ∧ τ
14 10 13 orbi12d ⊢ φ → ψ ∧ χ ∨ ¬ ψ ∧ χ ↔ ψ ∧ θ ∨ ¬ ψ ∧ τ
15 5 7 14 3bitrd ⊢ φ → χ ↔ ψ ∧ θ ∨ ¬ ψ ∧ τ