This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infeq123d

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

Ref Expression
Hypotheses infeq123d.a ⊢ φ → A = D
infeq123d.b ⊢ φ → B = E
infeq123d.c ⊢ φ → C = F
Assertion infeq123d ⊢ φ → inf A B C = inf D E F

Proof

Step Hyp Ref Expression
1 infeq123d.a ⊢ φ → A = D
2 infeq123d.b ⊢ φ → B = E
3 infeq123d.c ⊢ φ → C = F
4 3 cnveqd ⊢ φ → C -1 = F -1
5 1 2 4 supeq123d ⊢ φ → sup A B C -1 = sup D E F -1
6 df-inf ⊢ inf A B C = sup A B C -1
7 df-inf ⊢ inf D E F = sup D E F -1
8 5 6 7 3eqtr4g ⊢ φ → inf A B C = inf D E F