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

Metamath Proof Explorer

Theorem ifbieq1d

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018)

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

Proof

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