Theorem aecoms-o

Description: A commutation rule for identical variable specifiers. Version of aecoms using ax-c11 . (Contributed by NM, 10-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	alequcoms-o.1	|- ( A. x x = y -> ph )
Assertion	aecoms-o	|- ( A. y y = x -> ph )

Proof

Step	Hyp	Ref	Expression
1		alequcoms-o.1	|- ( A. x x = y -> ph )
2		aecom-o	|- ( A. y y = x -> A. x x = y )
3	2 1	syl	|- ( A. y y = x -> ph )