Metamath Proof Explorer

Theorem ifeq1da

Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypothesis ifeq1da.1 ⊢ φ ∧ ψ → A = B
Assertion ifeq1da ⊢ φ → if ψ A C = if ψ B C

Proof

Step Hyp Ref Expression
1 ifeq1da.1 ⊢ φ ∧ ψ → A = B
2 1 ifeq1d ⊢ φ ∧ ψ → if ψ A C = if ψ B C
3 iffalse ⊢ ¬ ψ → if ψ A C = C
4 iffalse ⊢ ¬ ψ → if ψ B C = C
5 3 4 eqtr4d ⊢ ¬ ψ → if ψ A C = if ψ B C
6 5 adantl ⊢ φ ∧ ¬ ψ → if ψ A C = if ψ B C
7 2 6 pm2.61dan ⊢ φ → if ψ A C = if ψ B C