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

Metamath Proof Explorer

Theorem ifbieq2i

Description: Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Hypotheses ifbieq2i.1 ⊢ φ ↔ ψ
ifbieq2i.2 ⊢ A = B
Assertion ifbieq2i ⊢ if φ C A = if ψ C B

Proof

Step Hyp Ref Expression
1 ifbieq2i.1 ⊢ φ ↔ ψ
2 ifbieq2i.2 ⊢ A = B
3 ifbi ⊢ φ ↔ ψ → if φ C A = if ψ C A
4 1 3 ax-mp ⊢ if φ C A = if ψ C A
5 ifeq2 ⊢ A = B → if ψ C A = if ψ C B
6 2 5 ax-mp ⊢ if ψ C A = if ψ C B
7 4 6 eqtri ⊢ if φ C A = if ψ C B