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  2117  elequ1  2118  ax9  2125  elequ2  2126  stdpc7  2253  sbequ12r  2255  cbvalv1  2341  cbval  2398  sb9  2519  ax9ALT  2726  sbralieALT  3319  rabrabi  3414  reurab  3660  reu8  3692  sbcco2  3768  reu8nf  3828  notabw  4263  sbcop1  5428  opeliunxp  5683  opeliun2xp  5684  elrnmpt1  5900  elidinxp  5993  fvn0ssdmfun  7007  elabrex  7176  elabrexg  7177  riotarab  7345  tfisi  7789  tfinds2  7794  opabex3d  7897  opabex3rd  7898  opabex3  7899  xpord2indlem  8077  xpord3inddlem  8084  mpocurryd  8199  boxriin  8864  ixpiunwdom  9476  elirrv  9483  elirrvOLD  9484  rabssnn0fi  13890  fproddivf  15891  prmodvdslcmf  16956  eqg0subg  19106  1mavmul  22461  ptbasfi  23494  elmptrab  23740  pcoass  24949  iundisj2  25475  dchrisumlema  27424  dchrisumlem2  27426  cusgrfilem2  29433  frgrncvvdeq  30284  frgr2wwlk1  30304  iundisj2f  32565  iundisj2fi  32774  bnj1014  34968  cvmsss2  35306  gonarlem  35426  ax8dfeq  35831  in-ax8  36257  ss-ax8  36258  bj-ssbid1ALT  36698  bj-cbvexw  36709  bj-sb  36720  finxpreclem6  37429  ralssiun  37440  wl-nfs1t  37570  wl-equsb4  37590  wl-euequf  37607  wl-ax11-lem8  37625  matunitlindflem1  37655  poimirlem26  37685  mblfinlem2  37697  sdclem2  37781  axc11-o  38989  evl1gprodd  42149  idomnnzgmulnz  42165  abbibw  42709  rexzrexnn0  42836  disjinfi  45228  dvnmptdivc  45975  iblsplitf  46007  vonn0ioo2  46727  vonn0icc2  46729  funressnvmo  47075  ichcircshi  47484  ichreuopeq  47503  paireqne  47541  reuopreuprim  47556  uspgrsprf1  48177