Theorem alequcoms 1503

Description: A commutation rule for identical variable specifiers.

Hypothesis

Ref	Expression
alequcoms.1	|- (A.x x = y -> ph)

Assertion

Ref	Expression
alequcoms	|- (A.y y = x -> ph)

Proof of Theorem alequcoms

Step	Hyp	Ref	Expression
1		alequcom 1502	. 2 |- (A.y y = x -> A.x x = y)
2		alequcoms.1	. 2 |- (A.x x = y -> ph)
3	1, 2	syl 12	1 |- (A.y y = x -> ph)

Syntax hints:   -> wi 3  A.wal 1296   = wceq 1298

This theorem is referenced by:  hbae 1505  dvelimfALT 1514  dral1 1515  aev 1577  sbequi 1598  hbsb4 1620  ax11indalem 1759  ax11inda2ALT 1760  a12stdy4 1766  hbeu 1782  nd4 6093  axrepnd 6098  axpowndlem3 6103  axpownd 6105  axregnd 6108  axinfnd 6110  axacndlem5 6115  axacnd 6116

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-10 1308

Copyright terms: Public domain