Theorem alequcoms 1141

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 1140	. 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 952   = wceq 954

This theorem is referenced by:  hbae 1143  dvelimfALT 1151  dral1 1152  sbequi 1226  hbsb4 1246  ax11indalem 1366  ax11inda2ALT 1367  a12stdy4 1373  hbeu 1387  nd4 4921  axrepnd 4926  axpowndlem3 4931  axpownd 4933  axregnd 4936  axinfnd 4938  axacndlem5 4943  axacnd 4944

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

Copyright terms: Public domain