Metamath Proof Explorer


Theorem ifbieq12i

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 ( 𝜓 , 𝐶 , 𝐷 )

Proof

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 ( 𝜓 , 𝐶 , 𝐷 )