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

Metamath Proof Explorer

Theorem caovassd

Description: Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses caovassg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x F y F z = x F y F z
caovassd.2 ⊢ φ → A ∈ S
caovassd.3 ⊢ φ → B ∈ S
caovassd.4 ⊢ φ → C ∈ S
Assertion caovassd ⊢ φ → A F B F C = A F B F C

Proof

Step Hyp Ref Expression
1 caovassg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x F y F z = x F y F z
2 caovassd.2 ⊢ φ → A ∈ S
3 caovassd.3 ⊢ φ → B ∈ S
4 caovassd.4 ⊢ φ → C ∈ S
5 id ⊢ φ → φ
6 1 caovassg ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ S → A F B F C = A F B F C
7 5 2 3 4 6 syl13anc ⊢ φ → A F B F C = A F B F C