Theorem infeq1i

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

	Ref	Expression
Hypothesis	infeq1i.1	|- B = C
Assertion	infeq1i	|- inf ( B , A , R ) = inf ( C , A , R )

Proof

Step	Hyp	Ref	Expression
1		infeq1i.1	|- B = C
2		infeq1	|- ( B = C -> inf ( B , A , R ) = inf ( C , A , R ) )
3	1 2	ax-mp	|- inf ( B , A , R ) = inf ( C , A , R )