Theorem infeq123d

Description: Equality deduction for infimum. (Contributed by AV, 2-Sep-2020)

	Ref	Expression
Hypotheses	infeq123d.a	|- ( ph -> A = D )
	infeq123d.b	|- ( ph -> B = E )
	infeq123d.c	|- ( ph -> C = F )
Assertion	infeq123d	|- ( ph -> inf ( A , B , C ) = inf ( D , E , F ) )

Proof

Step	Hyp	Ref	Expression
1		infeq123d.a	|- ( ph -> A = D )
2		infeq123d.b	|- ( ph -> B = E )
3		infeq123d.c	|- ( ph -> C = F )
4	3	cnveqd	|- ( ph -> `' C = `' F )
5	1 2 4	supeq123d	|- ( ph -> sup ( A , B , `' C ) = sup ( D , E , `' F ) )
6		df-inf	|- inf ( A , B , C ) = sup ( A , B , `' C )
7		df-inf	|- inf ( D , E , F ) = sup ( D , E , `' F )
8	5 6 7	3eqtr4g	|- ( ph -> inf ( A , B , C ) = inf ( D , E , F ) )