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φAifψBC=A→χ↔θ
elim2if.2 ⊢ifφAifψBC=B→χ↔τ
elim2if.3 ⊢ifφAifψBC=C→χ↔η
Assertion elim2if ⊢χ↔φ∧θ∨¬φ∧ψ∧τ∨¬ψ∧η

Proof

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