Theorem equcoms 1845

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 1843	. 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 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839

This theorem depends on definitions:  df-bi 188  df-ex 1660

This theorem is referenced by:  equtr  1846  stdpc7  1851  equtr2  1852  ax13b  1855  spfw  1856  cbvalw  1858  alcomiw  1861  elequ1  1871  elequ2  1873  19.8a  1908  19.8aOLD  1909  sbequ12r  2048  cbval  2075  sbequ  2170  sb9  2220  euequ1  2271  cleqhOLD  2538  cbvabOLD  2564  reu8  3267  sbcco2  3323  opeliunxp  4901  elrnmpt1  5098  iotaval  5572  fvn0ssdmfun  6024  elabrex  6159  snnex  6607  tfisi  6695  tfinds2  6700  opabex3d  6781  opabex3  6782  mpt2curryd  7020  boxriin  7568  ixpiunwdom  8108  elirrv  8114  rabssnn0fi  12197  fproddivf  14026  prmodvdslcmf  14990  prmordvdslcmfOLD  15004  prmordvdslcmsOLDOLD  15006  imasvscafn  15428  1mavmul  19557  ptbasfi  20580  elmptrab  20826  pcoass  22039  iundisj2  22486  dchrisumlema  24310  dchrisumlem2  24312  cusgrafilem2  25191  frgrancvvdeqlem9  25752  iundisj2f  28187  iundisj2fi  28364  bnj1014  29764  cvmsss2  29990  ax8dfeq  30437  bj-cbvexw  31220  bj-cbvalv  31281  bj-cleqh  31342  wl-nfs1t  31782  wl-equsb4  31796  wl-euequ1f  31814  wl-19.8a  31821  wl-ax11-lem8  31833  poimirlem26  31877  mblfinlem2  31889  sdclem2  31982  ax13fromc9  32392  axc11-o  32438  rexzrexnn0  35563  elabrexg  37228  disjinfi  37315  iblsplitf  37664  opeliun2xp  39302