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  3697  reu8  3729  sbcco2  3804  reu8nf  3871  notabw  4303  ab0OLD  4375  sbcop1  5488  opeliunxp  5742  elrnmpt1  5956  elidinxp  6042  fvn0ssdmfun  7074  elabrex  7239  riotarab  7405  tfisi  7845  tfinds2  7850  opabex3d  7949  opabex3rd  7950  opabex3  7951  xpord2indlem  8130  xpord3inddlem  8137  mpocurryd  8251  boxriin  8931  ixpiunwdom  9582  elirrv  9588  rabssnn0fi  13948  fproddivf  15928  prmodvdslcmf  16977  eqg0subg  19068  1mavmul  22042  ptbasfi  23077  elmptrab  23323  pcoass  24532  iundisj2  25058  dchrisumlema  26981  dchrisumlem2  26983  cusgrfilem2  28703  frgrncvvdeq  29552  frgr2wwlk1  29572  iundisj2f  31809  iundisj2fi  31996  bnj1014  33961  cvmsss2  34254  gonarlem  34374  ax8dfeq  34759  bj-ssbid1ALT  35531  bj-cbvexw  35542  bj-sb  35554  finxpreclem6  36266  ralssiun  36277  wl-nfs1t  36395  wl-equsb4  36411  wl-euequf  36428  wl-ax11-lem8  36443  matunitlindflem1  36473  poimirlem26  36503  mblfinlem2  36515  sdclem2  36599  axc11-o  37810  rexzrexnn0  41528  elabrexg  43714  disjinfi  43877  dvnmptdivc  44641  iblsplitf  44673  vonn0ioo2  45393  vonn0icc2  45395  funressnvmo  45742  ichcircshi  46109  ichreuopeq  46128  paireqne  46166  reuopreuprim  46181  uspgrsprf1  46512  opeliun2xp  46962