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  2255  sbequ12r  2257  cbvalv1  2343  cbval  2400  sb9  2521  ax9ALT  2728  sbralieALT  3320  rabrabi  3415  reurab  3656  reu8  3688  sbcco2  3764  reu8nf  3824  notabw  4262  sbcop1  5431  opeliunxp  5686  opeliun2xp  5687  elrnmpt1  5904  elidinxp  5997  fvn0ssdmfun  7013  elabrex  7182  elabrexg  7183  riotarab  7351  tfisi  7795  tfinds2  7800  opabex3d  7903  opabex3rd  7904  opabex3  7905  xpord2indlem  8083  xpord3inddlem  8090  mpocurryd  8205  boxriin  8870  ixpiunwdom  9483  elirrv  9490  elirrvOLD  9491  rabssnn0fi  13895  fproddivf  15896  prmodvdslcmf  16961  eqg0subg  19110  1mavmul  22464  ptbasfi  23497  elmptrab  23743  pcoass  24952  iundisj2  25478  dchrisumlema  27427  dchrisumlem2  27429  cusgrfilem2  29437  frgrncvvdeq  30291  frgr2wwlk1  30311  iundisj2f  32572  iundisj2fi  32784  bnj1014  34994  cvmsss2  35339  gonarlem  35459  ax8dfeq  35861  in-ax8  36289  ss-ax8  36290  bj-ssbid1ALT  36730  bj-cbvexw  36741  bj-sb  36752  finxpreclem6  37461  ralssiun  37472  wl-nfs1t  37602  wl-equsb4  37622  wl-euequf  37639  matunitlindflem1  37676  poimirlem26  37706  mblfinlem2  37718  sdclem2  37802  axc11-o  39070  evl1gprodd  42230  idomnnzgmulnz  42246  abbibw  42795  rexzrexnn0  42921  disjinfi  45313  dvnmptdivc  46060  iblsplitf  46092  vonn0ioo2  46812  vonn0icc2  46814  funressnvmo  47169  ichcircshi  47578  ichreuopeq  47597  paireqne  47635  reuopreuprim  47650  uspgrsprf1  48271