This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ifeq12da

Description: Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021)

Ref Expression
Hypotheses ifeq12da.1 ⊢ φ ∧ ψ → A = C
ifeq12da.2 ⊢ φ ∧ ¬ ψ → B = D
Assertion ifeq12da ⊢ φ → if ψ A B = if ψ C D

Proof

Step Hyp Ref Expression
1 ifeq12da.1 ⊢ φ ∧ ψ → A = C
2 ifeq12da.2 ⊢ φ ∧ ¬ ψ → B = D
3 1 ifeq1da ⊢ φ → if ψ A B = if ψ C B
4 iftrue ⊢ ψ → if ψ C B = C
5 iftrue ⊢ ψ → if ψ C D = C
6 4 5 eqtr4d ⊢ ψ → if ψ C B = if ψ C D
7 3 6 sylan9eq ⊢ φ ∧ ψ → if ψ A B = if ψ C D
8 2 ifeq2da ⊢ φ → if ψ A B = if ψ A D
9 iffalse ⊢ ¬ ψ → if ψ A D = D
10 iffalse ⊢ ¬ ψ → if ψ C D = D
11 9 10 eqtr4d ⊢ ¬ ψ → if ψ A D = if ψ C D
12 8 11 sylan9eq ⊢ φ ∧ ¬ ψ → if ψ A B = if ψ C D
13 7 12 pm2.61dan ⊢ φ → if ψ A B = if ψ C D