Theorem equcoms 1129

Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.

Hypothesis

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

Assertion

Ref	Expression
equcoms	|- (y = x -> ph)

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1127	. 2 |- (y = x -> x = y)
2		equcoms.1	. 2 |- (x = y -> ph)
3	1, 2	syl 10	1 |- (y = x -> ph)

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  equtr 1130  equequ2 1134  elequ1 1135  elequ2 1136  ax10o 1138  equvini 1167  stdpc7 1180  sbequ12a 1183  sbequ 1229  drsb2 1230  sb6rf 1260  sb6a 1337  mo 1393  tfinds2 3162  oprabval4g 4028  elirrv 4585  uninqs 10435

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-8 963  ax-12 967  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122

Copyright terms: Public domain