Theorem caovcomd

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

	Ref	Expression
Hypotheses	caovcomg.1	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
	caovcomd.2	|- ( ph -> A e. S )
	caovcomd.3	|- ( ph -> B e. S )
Assertion	caovcomd	|- ( ph -> ( A F B ) = ( B F A ) )

Proof

Step	Hyp	Ref	Expression
1		caovcomg.1	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
2		caovcomd.2	|- ( ph -> A e. S )
3		caovcomd.3	|- ( ph -> B e. S )
4		id	|- ( ph -> ph )
5	1	caovcomg	|- ( ( ph /\ ( A e. S /\ B e. S ) ) -> ( A F B ) = ( B F A ) )
6	4 2 3 5	syl12anc	|- ( ph -> ( A F B ) = ( B F A ) )