Theorem ifbieq1d

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

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

Proof

Step	Hyp	Ref	Expression
1		ifbieq1d.1	|- ( ph -> ( ps <-> ch ) )
2		ifbieq1d.2	|- ( ph -> A = B )
3	1	ifbid	|- ( ph -> if ( ps , A , C ) = if ( ch , A , C ) )
4	2	ifeq1d	|- ( ph -> if ( ch , A , C ) = if ( ch , B , C ) )
5	3 4	eqtrd	|- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )