# Metamath Proof Explorer

## Theorem ibllem

Description: Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014)

Ref Expression
Hypothesis ibllem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}={C}$
Assertion ibllem ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)=if\left(\left({x}\in {A}\wedge 0\le {C}\right),{C},0\right)$

### Proof

Step Hyp Ref Expression
1 ibllem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}={C}$
2 1 breq2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(0\le {B}↔0\le {C}\right)$
3 2 pm5.32da ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge 0\le {B}\right)↔\left({x}\in {A}\wedge 0\le {C}\right)\right)$
4 3 ifbid ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)=if\left(\left({x}\in {A}\wedge 0\le {C}\right),{B},0\right)$
5 1 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge 0\le {C}\right)\right)\to {B}={C}$
6 5 ifeq1da ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le {C}\right),{B},0\right)=if\left(\left({x}\in {A}\wedge 0\le {C}\right),{C},0\right)$
7 4 6 eqtrd ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)=if\left(\left({x}\in {A}\wedge 0\le {C}\right),{C},0\right)$