Theorem infeq1d

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

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

Proof

Step	Hyp	Ref	Expression
1		infeq1d.1	|- ( ph -> B = C )
2		infeq1	|- ( B = C -> inf ( B , A , R ) = inf ( C , A , R ) )
3	1 2	syl	|- ( ph -> inf ( B , A , R ) = inf ( C , A , R ) )