Theorem eq4s 822

Description: A commutation rule for identical variable specifiers.

Hypothesis

Ref	Expression
eq4s.1	⊢ (∀x x = y → φ)

Assertion

Ref	Expression
eq4s	⊢ (∀y y = x → φ)

Proof of Theorem eq4s

Step	Hyp	Ref	Expression
1		eq4 821	. 2 ⊢ (∀y y = x → ∀x x = y)
2		eq4s.1	. 2 ⊢ (∀x x = y → φ)
3	1, 2	syl 12	1 ⊢ (∀y y = x → φ)

Syntax hints:   → wi 2  ∀wal 672   = weq 797

This theorem is referenced by:  eq5 824  del35 836  del43 856  del43b 857  sb6y 872  hbsb3 875  sbequi 876  hbsb4 905  ddelimf2 907  hbeu 1016  nd4 3735  axrepnd 3740  axpowndlem3 3745  axpownd 3747  axregnd 3750  axinfnd 3752  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org