Theorem equcoms 1896

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	⊢ (𝑥 = 𝑦 → 𝜑)

Assertion

Ref	Expression
equcoms	⊢ (𝑦 = 𝑥 → 𝜑)

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1893	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 17	1 ⊢ (𝑦 = 𝑥 → 𝜑)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883

This theorem depends on definitions:  df-bi 192  df-an 380  df-ex 1693

This theorem is referenced by:  equtr  1897  equeuclr  1899  equtr2OLD  1905  stdpc7  1907  equvinvOLD  1911  spfw  1914  cbvalw  1916  alcomiw  1919  ax8  1943  elequ1  1944  ax9  1950  elequ2  1951  19.8aOLD  1989  cbvalv1  2116  sbequ12r  2132  cbval  2161  sbequ  2259  sb9  2309  reu8  3258  sbcco2  3315  opeliunxp  4933  elrnmpt1  5132  iotaval  5608  fvn0ssdmfun  6080  elabrex  6219  snnex  6674  tfisi  6762  tfinds2  6767  opabex3d  6848  opabex3  6849  mpt2curryd  7093  boxriin  7647  ixpiunwdom  8189  elirrv  8197  rabssnn0fi  12312  fproddivf  14201  prmodvdslcmf  15167  prmordvdslcmfOLD  15181  prmordvdslcmsOLDOLD  15183  imasvscafn  15608  1mavmul  19731  ptbasfi  20753  elmptrab  20999  pcoass  22214  iundisj2  22662  dchrisumlema  24487  dchrisumlem2  24489  cusgrafilem2  25369  frgrancvvdeqlem9  25929  iundisj2f  28359  iundisj2fi  28529  bnj1014  29923  cvmsss2  30149  ax8dfeq  30596  bj-ssbid1ALT  31443  bj-cbvexw  31457  bj-sb  31465  finxpreclem6  32009  wl-nfs1t  32102  wl-equsb4  32116  wl-euequ1f  32134  wl-ax11-lem8  32147  matunitlindflem1  32174  poimirlem26  32204  mblfinlem2  32216  sdclem2  32308  ax13fromc9  32709  axc11-o  32755  rexzrexnn0  35887  elabrexg  37716  disjinfi  37828  dvnmptdivc  38232  iblsplitf  38266  vonn0ioo2  38976  vonn0icc2  38978  cusgrfilem2  40072  frgrncvvdeq  40880  opeliun2xp  41304