Theorem equcoms 2021

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 2018	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  equtr  2022  equeuclr  2024  spfw  2034  cbvalw  2036  alcomimw  2044  ax8  2119  elequ1  2120  ax9  2127  elequ2  2128  stdpc7  2257  sbequ12r  2259  cbvalv1  2345  cbval  2402  sb9  2523  ax9ALT  2731  sbralieALT  3323  rabrabi  3418  reurab  3659  reu8  3691  sbcco2  3767  reu8nf  3827  notabw  4265  sbcop1  5436  opeliunxp  5691  opeliun2xp  5692  elrnmpt1  5909  elidinxp  6003  fvn0ssdmfun  7019  elabrex  7188  elabrexg  7189  riotarab  7357  tfisi  7801  tfinds2  7806  opabex3d  7909  opabex3rd  7910  opabex3  7911  xpord2indlem  8089  xpord3inddlem  8096  mpocurryd  8211  boxriin  8878  ixpiunwdom  9495  elirrv  9502  elirrvOLD  9503  rabssnn0fi  13909  fproddivf  15910  prmodvdslcmf  16975  eqg0subg  19125  1mavmul  22492  ptbasfi  23525  elmptrab  23771  pcoass  24980  iundisj2  25506  dchrisumlema  27455  dchrisumlem2  27457  cusgrfilem2  29530  frgrncvvdeq  30384  frgr2wwlk1  30404  iundisj2f  32665  iundisj2fi  32877  bnj1014  35117  cvmsss2  35468  gonarlem  35588  ax8dfeq  35990  in-ax8  36418  ss-ax8  36419  bj-ssbid1ALT  36866  bj-cbvexw  36877  bj-sb  36888  finxpreclem6  37597  ralssiun  37608  wl-nfs1t  37738  wl-equsb4  37758  wl-euequf  37775  matunitlindflem1  37813  poimirlem26  37843  mblfinlem2  37855  sdclem2  37939  axc11-o  39207  evl1gprodd  42367  idomnnzgmulnz  42383  abbibw  42916  rexzrexnn0  43042  disjinfi  45432  dvnmptdivc  46178  iblsplitf  46210  vonn0ioo2  46930  vonn0icc2  46932  funressnvmo  47287  ichcircshi  47696  ichreuopeq  47715  paireqne  47753  reuopreuprim  47768  uspgrsprf1  48389