Theorem equcoms 2024

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 2021	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  equtr  2025  equeuclr  2027  spfw  2037  cbvalw  2039  alcomiw  2047  ax8  2113  elequ1  2114  ax9  2121  elequ2  2122  stdpc7  2243  sbequ12r  2245  cbvalv1  2338  cbval  2398  sb9  2519  ax9ALT  2728  sbralieALT  3356  rabrabi  3451  reurab  3698  reu8  3730  sbcco2  3805  reu8nf  3872  notabw  4304  ab0OLD  4376  sbcop1  5489  opeliunxp  5744  elrnmpt1  5958  elidinxp  6044  fvn0ssdmfun  7077  elabrex  7242  riotarab  7408  tfisi  7848  tfinds2  7853  opabex3d  7952  opabex3rd  7953  opabex3  7954  xpord2indlem  8133  xpord3inddlem  8140  mpocurryd  8254  boxriin  8934  ixpiunwdom  9585  elirrv  9591  rabssnn0fi  13951  fproddivf  15931  prmodvdslcmf  16980  eqg0subg  19073  1mavmul  22050  ptbasfi  23085  elmptrab  23331  pcoass  24540  iundisj2  25066  dchrisumlema  26991  dchrisumlem2  26993  cusgrfilem2  28713  frgrncvvdeq  29562  frgr2wwlk1  29582  iundisj2f  31821  iundisj2fi  32008  bnj1014  33972  cvmsss2  34265  gonarlem  34385  ax8dfeq  34770  bj-ssbid1ALT  35542  bj-cbvexw  35553  bj-sb  35565  finxpreclem6  36277  ralssiun  36288  wl-nfs1t  36406  wl-equsb4  36422  wl-euequf  36439  wl-ax11-lem8  36454  matunitlindflem1  36484  poimirlem26  36514  mblfinlem2  36526  sdclem2  36610  axc11-o  37821  rexzrexnn0  41542  elabrexg  43728  disjinfi  43891  dvnmptdivc  44654  iblsplitf  44686  vonn0ioo2  45406  vonn0icc2  45408  funressnvmo  45755  ichcircshi  46122  ichreuopeq  46141  paireqne  46179  reuopreuprim  46194  uspgrsprf1  46525  opeliun2xp  47008