Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ifbieq12i.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
ifbieq12i.2 | ⊢ 𝐴 = 𝐶 | ||
ifbieq12i.3 | ⊢ 𝐵 = 𝐷 | ||
Assertion | ifbieq12i | ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifbieq12i.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
2 | ifbieq12i.2 | ⊢ 𝐴 = 𝐶 | |
3 | ifbieq12i.3 | ⊢ 𝐵 = 𝐷 | |
4 | ifeq1 | ⊢ ( 𝐴 = 𝐶 → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐶 , 𝐵 ) ) | |
5 | 2 4 | ax-mp | ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐶 , 𝐵 ) |
6 | 1 3 | ifbieq2i | ⊢ if ( 𝜑 , 𝐶 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) |
7 | 5 6 | eqtri | ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) |