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

Metamath Proof Explorer

Theorem ifbieq12d

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step Hyp Ref Expression
1 ifbieq12d.1 ⊢ φ → ψ ↔ χ
2 ifbieq12d.2 ⊢ φ → A = C
3 ifbieq12d.3 ⊢ φ → B = D
4 1 ifbid ⊢ φ → if ψ A B = if χ A B
5 2 3 ifeq12d ⊢ φ → if χ A B = if χ C D
6 4 5 eqtrd ⊢ φ → if ψ A B = if χ C D