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

Metamath Proof Explorer

Theorem ifeq2da

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

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

Proof

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