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

Metamath Proof Explorer

Theorem ifbieq12i

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

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

Proof

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