Metamath Proof Explorer


Theorem ifbieq12d

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

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