Metamath Proof Explorer

Theorem caovass

Description: Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 26-May-2014)

Ref Expression
Hypotheses caovass.1 ⊢A∈V
caovass.2 ⊢B∈V
caovass.3 ⊢C∈V
caovass.4 ⊢xFyFz=xFyFz
Assertion caovass ⊢AFBFC=AFBFC

Proof

Step Hyp Ref Expression
1 caovass.1 ⊢A∈V
2 caovass.2 ⊢B∈V
3 caovass.3 ⊢C∈V
4 caovass.4 ⊢xFyFz=xFyFz
5 tru ⊢⊤
6 4 a1i ⊢⊤∧x∈V∧y∈V∧z∈V→xFyFz=xFyFz
7 6 caovassg ⊢⊤∧A∈V∧B∈V∧C∈V→AFBFC=AFBFC
8 5 7 mpan ⊢A∈V∧B∈V∧C∈V→AFBFC=AFBFC
9 1 2 3 8 mp3an ⊢AFBFC=AFBFC