Theorem ifbieq2i

Description: Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Hypotheses	ifbieq2i.1	|- ( ph <-> ps )
	ifbieq2i.2	|- A = B
Assertion	ifbieq2i	|- if ( ph , C , A ) = if ( ps , C , B )

Proof

Step	Hyp	Ref	Expression
1		ifbieq2i.1	|- ( ph <-> ps )
2		ifbieq2i.2	|- A = B
3		ifbi	|- ( ( ph <-> ps ) -> if ( ph , C , A ) = if ( ps , C , A ) )
4	1 3	ax-mp	|- if ( ph , C , A ) = if ( ps , C , A )
5		ifeq2	|- ( A = B -> if ( ps , C , A ) = if ( ps , C , B ) )
6	2 5	ax-mp	|- if ( ps , C , A ) = if ( ps , C , B )
7	4 6	eqtri	|- if ( ph , C , A ) = if ( ps , C , B )