Theorem equcoms 1132

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 1130	. 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 958

This theorem is referenced by:  equtr 1133  equequ2 1137  elequ1 1138  elequ2 1139  ax10o 1141  equvini 1170  stdpc7 1182  sbequ12a 1185  sbequ 1231  drsb2 1232  sb6rf 1262  sb6a 1339  mo 1395  tfinds2 3171  oprabval4g 4037  elirrv 4607  uninqs 10436

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-8 966  ax-12 970  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

Copyright terms: Public domain