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

Metamath Proof Explorer

Theorem ifeq1d

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

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

Proof

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