Theorem equcoms 2022

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 2019	. 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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  equtr  2023  equeuclr  2025  spfw  2035  cbvalw  2037  alcomimw  2045  ax8  2120  elequ1  2121  ax9  2128  elequ2  2129  stdpc7  2258  sbequ12r  2260  cbvalv1  2345  cbval  2402  sb9  2523  ax9ALT  2731  sbralieALT  3316  rabrabi  3408  reurab  3647  reu8  3679  sbcco2  3755  reu8nf  3815  notabw  4253  sbcop1  5441  opeliunxp  5698  opeliun2xp  5699  elrnmpt1  5915  elidinxp  6009  fvn0ssdmfun  7026  elabrex  7197  elabrexg  7198  riotarab  7366  tfisi  7810  tfinds2  7815  opabex3d  7918  opabex3rd  7919  opabex3  7920  xpord2indlem  8097  xpord3inddlem  8104  mpocurryd  8219  boxriin  8888  ixpiunwdom  9505  elirrv  9512  elirrvOLD  9513  rabssnn0fi  13948  fproddivf  15952  prmodvdslcmf  17018  eqg0subg  19171  1mavmul  22513  ptbasfi  23546  elmptrab  23792  pcoass  24991  iundisj2  25516  dchrisumlema  27451  dchrisumlem2  27453  cusgrfilem2  29525  frgrncvvdeq  30379  frgr2wwlk1  30399  iundisj2f  32660  iundisj2fi  32870  bnj1014  35103  cvmsss2  35456  gonarlem  35576  ax8dfeq  35978  in-ax8  36406  ss-ax8  36407  bj-ssbid1ALT  36959  bj-cbvexw  36971  bj-sb  36984  bj-axseprep  37381  finxpreclem6  37712  ralssiun  37723  wl-nfs1t  37862  wl-equsb4  37882  wl-euequf  37899  matunitlindflem1  37937  poimirlem26  37967  mblfinlem2  37979  sdclem2  38063  axc11-o  39397  evl1gprodd  42556  idomnnzgmulnz  42572  abbibw  43110  rexzrexnn0  43232  disjinfi  45622  dvnmptdivc  46366  iblsplitf  46398  vonn0ioo2  47118  vonn0icc2  47120  funressnvmo  47493  ichcircshi  47914  ichreuopeq  47933  paireqne  47971  reuopreuprim  47986  nprmmul3  47989  uspgrsprf1  48623