Metamath Proof Explorer


Theorem ifbieq1d

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018)

Ref Expression
Hypotheses ifbieq1d.1 ( 𝜑 → ( 𝜓𝜒 ) )
ifbieq1d.2 ( 𝜑𝐴 = 𝐵 )
Assertion ifbieq1d ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐶 ) = if ( 𝜒 , 𝐵 , 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ifbieq1d.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 ifbieq1d.2 ( 𝜑𝐴 = 𝐵 )
3 1 ifbid ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐶 ) = if ( 𝜒 , 𝐴 , 𝐶 ) )
4 2 ifeq1d ( 𝜑 → if ( 𝜒 , 𝐴 , 𝐶 ) = if ( 𝜒 , 𝐵 , 𝐶 ) )
5 3 4 eqtrd ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐶 ) = if ( 𝜒 , 𝐵 , 𝐶 ) )