Theorem equcoms 1735

Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)

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 1733	. 2 |- ( y = x -> x = y )
2		equcoms.1	. 2 |- ( x = y -> ph )
3	1, 2	syl 16	1 |- ( y = x -> ph )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730

This theorem depends on definitions:  df-bi 185  df-ex 1588

This theorem is referenced by:  equtr  1736  stdpc7  1741  equtr2  1742  ax13b  1745  spfw  1746  cbvalw  1748  alcomiw  1751  elequ1  1761  elequ2  1763  19.8a  1795  sbequ12r  1946  sbequ12aOLD  1948  cbval  1978  sbequ  2074  sb6rfOLD  2130  sb9  2133  sb6aOLD  2163  ax13fromc9  2213  axc11-o  2259  euequ1  2266  moOLD  2312  cleqhOLD  2567  cbvabOLD  2593  reu8  3255  sbcco2  3311  opeliunxp  4991  elrnmpt1  5189  iotaval  5493  elabrex  6062  snnex  6485  tfisi  6572  tfinds2  6577  opabex3d  6658  opabex3  6659  mpt2curryd  6891  boxriin  7408  ixpiunwdom  7910  elirrv  7916  imasvscafn  14586  1mavmul  18479  ptbasfi  19279  elmptrab  19525  pcoass  20721  iundisj2  21156  dchrisumlema  22863  dchrisumlem2  22865  cusgrafilem2  23533  iundisj2f  26076  iundisj2fi  26219  voliune  26782  volfiniune  26783  cvmsss2  27300  ax8dfeq  27749  wl-nfs1t  28508  wl-equsb4  28522  wl-ax11-lem8  28549  mblfinlem2  28570  sdclem2  28779  rexzrexnn0  29283  frgrancvvdeqlem9  30775  opeliun2xp  30861  rabssnn0fi  30888  bnj1014  32256  bj-cbvalv  32535  bj-cleqh  32596