Theorem equcoms 1934

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 1931	. 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 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  equtr  1935  equeuclr  1937  equtr2OLD  1943  stdpc7  1945  equvinvOLD  1949  spfw  1952  spfwOLD  1953  cbvalw  1955  alcomiw  1958  ax8  1983  elequ1  1984  ax9  1990  elequ2  1991  19.8aOLD  2040  sbequ12r  2098  cbvalv1  2163  cbval  2259  cbvalv  2261  sbequ  2364  sb9  2414  reu8  3369  sbcco2  3426  opeliunxp  5093  elrnmpt1  5295  iotaval  5779  fvn0ssdmfun  6258  elabrex  6405  snnex  6862  tfisi  6950  tfinds2  6955  opabex3d  7037  opabex3  7038  mpt2curryd  7282  boxriin  7836  ixpiunwdom  8379  elirrv  8387  rabssnn0fi  12647  fproddivf  14557  prmodvdslcmf  15589  imasvscafn  16020  1mavmul  20173  ptbasfi  21194  elmptrab  21440  pcoass  22632  iundisj2  23124  dchrisumlema  24977  dchrisumlem2  24979  cusgrafilem2  26008  frgrancvvdeqlem9  26568  iundisj2f  28785  iundisj2fi  28943  bnj1014  30284  cvmsss2  30510  ax8dfeq  30948  bj-ssbid1ALT  31837  bj-cbvexw  31851  bj-sb  31864  finxpreclem6  32409  wl-nfs1t  32503  wl-equsb4  32517  wl-euequ1f  32535  wl-ax11-lem8  32548  matunitlindflem1  32575  poimirlem26  32605  mblfinlem2  32617  sdclem2  32708  axc11-o  33254  rexzrexnn0  36386  elabrexg  38229  disjinfi  38375  dvnmptdivc  38828  iblsplitf  38862  vonn0ioo2  39581  vonn0icc2  39583  cusgrfilem2  40672  frgrncvvdeq  41480  opeliun2xp  41904