Theorem equcoms 1864

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 1861	. 2 |- ( y = x -> x = y )
2		equcoms.1	. 2 |- ( x = y -> ph )
3	1, 2	syl 17	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 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664

This theorem is referenced by:  equtr  1865  equtr2  1869  stdpc7  1871  ax13b  1874  spfw  1875  cbvalw  1877  alcomiw  1880  elequ1  1894  elequ2  1901  19.8a  1935  19.8aOLD  1936  cbvalv1  2064  sbequ12r  2084  cbval  2114  sbequ  2205  sb9  2255  euequ1  2305  reu8  3234  sbcco2  3291  opeliunxp  4886  elrnmpt1  5083  iotaval  5557  fvn0ssdmfun  6013  elabrex  6148  snnex  6597  tfisi  6685  tfinds2  6690  opabex3d  6771  opabex3  6772  mpt2curryd  7016  boxriin  7564  ixpiunwdom  8106  elirrv  8112  rabssnn0fi  12198  fproddivf  14041  prmodvdslcmf  15005  prmordvdslcmfOLD  15019  prmordvdslcmsOLDOLD  15021  imasvscafn  15443  1mavmul  19573  ptbasfi  20596  elmptrab  20842  pcoass  22055  iundisj2  22502  dchrisumlema  24326  dchrisumlem2  24328  cusgrafilem2  25208  frgrancvvdeqlem9  25769  iundisj2f  28200  iundisj2fi  28373  bnj1014  29771  cvmsss2  29997  ax8dfeq  30445  bj-ssbid1ALT  31261  bj-cbvexw  31273  finxpreclem6  31788  wl-nfs1t  31871  wl-equsb4  31885  wl-euequ1f  31903  wl-19.8a  31910  wl-ax11-lem8  31922  poimirlem26  31966  mblfinlem2  31978  sdclem2  32071  ax13fromc9  32476  axc11-o  32522  rexzrexnn0  35647  elabrexg  37370  disjinfi  37468  iblsplitf  37847  cusgrfilem2  39517  opeliun2xp  40167