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

Metamath Proof Explorer

Theorem ifeq2d

Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005)

Ref Expression
Hypothesis ifeq1d.1 ⊢ φ → A = B
Assertion ifeq2d ⊢ φ → if ψ C A = if ψ C B

Proof

Step Hyp Ref Expression
1 ifeq1d.1 ⊢ φ → A = B
2 ifeq2 ⊢ A = B → if ψ C A = if ψ C B
3 1 2 syl ⊢ φ → if ψ C A = if ψ C B