Theorem equcoms 1739

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 1737	. 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 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734

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

This theorem is referenced by:  equtr  1740  stdpc7  1745  equtr2  1746  ax13b  1749  spfw  1750  cbvalw  1752  alcomiw  1755  elequ1  1765  elequ2  1767  19.8a  1801  19.8aOLD  1802  sbequ12r  1955  sbequ12aOLD  1957  cbval  1987  sbequ  2083  sb6rfOLD  2139  sb9  2142  sb6aOLD  2171  ax13fromc9  2221  axc11-o  2267  euequ1  2274  moOLD  2320  cleqhOLD  2576  cbvabOLD  2602  reu8  3292  sbcco2  3348  opeliunxp  5043  elrnmpt1  5242  iotaval  5553  elabrex  6134  snnex  6577  tfisi  6664  tfinds2  6669  opabex3d  6752  opabex3  6753  mpt2curryd  6988  boxriin  7501  ixpiunwdom  8006  elirrv  8012  rabssnn0fi  12051  imasvscafn  14781  1mavmul  18810  ptbasfi  19810  elmptrab  20056  pcoass  21252  iundisj2  21687  dchrisumlema  23394  dchrisumlem2  23396  cusgrafilem2  24142  frgrancvvdeqlem9  24704  iundisj2f  27108  iundisj2fi  27256  voliune  27827  volfiniune  27828  cvmsss2  28345  ax8dfeq  28794  wl-nfs1t  29554  wl-equsb4  29568  wl-ax11-lem8  29595  mblfinlem2  29616  sdclem2  29825  rexzrexnn0  30328  elabrexg  30967  iblsplitf  31243  opeliun2xp  31861  bnj1014  32972  bj-cbvalv  33253  bj-cleqh  33314