Theorem alequcoms 1143

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 1142	. 2 |- (A.y y = x -> A.x x = y)
2		alequcoms.1	. 2 |- (A.x x = y -> ph)
3	1, 2	syl 10	1 |- (A.y y = x -> ph)

Syntax hints:   -> wi 3  A.wal 954   = wceq 956

This theorem is referenced by:  hbae 1145  dvelimfALT 1153  dral1 1154  sbequi 1228  hbsb4 1248  ax11indalem 1368  ax11inda2ALT 1369  a12stdy4 1375  hbeu 1389  nd4 4941  axrepnd 4946  axpowndlem3 4951  axpownd 4953  axregnd 4956  axinfnd 4958  axacndlem5 4963  axacnd 4964

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

Copyright terms: Public domain