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

Metamath Proof Explorer

Theorem ifbieq2d

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

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

Proof

Step Hyp Ref Expression
1 ifbieq2d.1 ⊢ φ → ψ ↔ χ
2 ifbieq2d.2 ⊢ φ → A = B
3 1 ifbid ⊢ φ → if ψ C A = if χ C A
4 2 ifeq2d ⊢ φ → if χ C A = if χ C B
5 3 4 eqtrd ⊢ φ → if ψ C A = if χ C B