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

Metamath Proof Explorer

Theorem ifbid

Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005)

Ref Expression
Hypothesis ifbid.1 ⊢ φ → ψ ↔ χ
Assertion ifbid ⊢ φ → if ψ A B = if χ A B

Proof

Step Hyp Ref Expression
1 ifbid.1 ⊢ φ → ψ ↔ χ
2 ifbi ⊢ ψ ↔ χ → if ψ A B = if χ A B
3 1 2 syl ⊢ φ → if ψ A B = if χ A B