Theorem equcoms 2023

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 2020	. 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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  equtr  2024  equeuclr  2026  spfw  2036  cbvalw  2038  alcomiw  2046  ax8  2112  elequ1  2113  ax9  2120  elequ2  2121  stdpc7  2242  sbequ12r  2244  cbvalv1  2337  cbval  2397  sb9  2518  ax9ALT  2727  sbralieALT  3355  rabrabi  3450  reurab  3697  reu8  3729  sbcco2  3804  reu8nf  3871  notabw  4303  ab0OLD  4375  sbcop1  5488  opeliunxp  5743  elrnmpt1  5957  elidinxp  6043  fvn0ssdmfun  7076  elabrex  7244  riotarab  7410  tfisi  7850  tfinds2  7855  opabex3d  7954  opabex3rd  7955  opabex3  7956  xpord2indlem  8135  xpord3inddlem  8142  mpocurryd  8256  boxriin  8936  ixpiunwdom  9587  elirrv  9593  rabssnn0fi  13953  fproddivf  15933  prmodvdslcmf  16982  eqg0subg  19075  1mavmul  22057  ptbasfi  23092  elmptrab  23338  pcoass  24547  iundisj2  25073  dchrisumlema  26998  dchrisumlem2  27000  cusgrfilem2  28751  frgrncvvdeq  29600  frgr2wwlk1  29620  iundisj2f  31859  iundisj2fi  32046  bnj1014  34041  cvmsss2  34334  gonarlem  34454  ax8dfeq  34839  bj-ssbid1ALT  35628  bj-cbvexw  35639  bj-sb  35651  finxpreclem6  36363  ralssiun  36374  wl-nfs1t  36492  wl-equsb4  36508  wl-euequf  36525  wl-ax11-lem8  36540  matunitlindflem1  36570  poimirlem26  36600  mblfinlem2  36612  sdclem2  36696  axc11-o  37907  rexzrexnn0  41624  elabrexg  43810  disjinfi  43970  dvnmptdivc  44733  iblsplitf  44765  vonn0ioo2  45485  vonn0icc2  45487  funressnvmo  45834  ichcircshi  46201  ichreuopeq  46220  paireqne  46258  reuopreuprim  46273  uspgrsprf1  46604  opeliun2xp  47087