Theorem infeq123d

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

	Ref	Expression
Hypotheses	infeq123d.a	$$⊢\phi \to A=D$$
	infeq123d.b	$$⊢\phi \to B=E$$
	infeq123d.c	$$⊢\phi \to C=F$$
Assertion	infeq123d	$$⊢\phi \to inf\left(A,B,C\right)=inf\left(D,E,F\right)$$

Proof

Step	Hyp	Ref	Expression
1		infeq123d.a	$$⊢\phi \to A=D$$
2		infeq123d.b	$$⊢\phi \to B=E$$
3		infeq123d.c	$$⊢\phi \to C=F$$
4	3	cnveqd	$$⊢\phi \to C^{-1}=F^{-1}$$
5	1 2 4	supeq123d	$$⊢\phi \to sup\left(A,B,C^{-1}\right)=sup\left(D,E,F^{-1}\right)$$
6		df-inf	$$⊢inf\left(A,B,C\right)=sup\left(A,B,C^{-1}\right)$$
7		df-inf	$$⊢inf\left(D,E,F\right)=sup\left(D,E,F^{-1}\right)$$
8	5 6 7	3eqtr4g	$$⊢\phi \to inf\left(A,B,C\right)=inf\left(D,E,F\right)$$