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  2346  cbval  2403  sb9  2524  ax9ALT  2732  sbralieALT  3317  rabrabi  3409  reurab  3648  reu8  3680  sbcco2  3756  reu8nf  3816  notabw  4254  sbcop1  5436  opeliunxp  5691  opeliun2xp  5692  elrnmpt1  5909  elidinxp  6003  fvn0ssdmfun  7020  elabrex  7190  elabrexg  7191  riotarab  7359  tfisi  7803  tfinds2  7808  opabex3d  7911  opabex3rd  7912  opabex3  7913  xpord2indlem  8090  xpord3inddlem  8097  mpocurryd  8212  boxriin  8881  ixpiunwdom  9498  elirrv  9505  elirrvOLD  9506  rabssnn0fi  13939  fproddivf  15943  prmodvdslcmf  17009  eqg0subg  19162  1mavmul  22523  ptbasfi  23556  elmptrab  23802  pcoass  25001  iundisj2  25526  dchrisumlema  27465  dchrisumlem2  27467  cusgrfilem2  29540  frgrncvvdeq  30394  frgr2wwlk1  30414  iundisj2f  32675  iundisj2fi  32885  bnj1014  35119  cvmsss2  35472  gonarlem  35592  ax8dfeq  35994  in-ax8  36422  ss-ax8  36423  bj-ssbid1ALT  36975  bj-cbvexw  36987  bj-sb  37000  bj-axseprep  37397  finxpreclem6  37726  ralssiun  37737  wl-nfs1t  37876  wl-equsb4  37896  wl-euequf  37913  matunitlindflem1  37951  poimirlem26  37981  mblfinlem2  37993  sdclem2  38077  axc11-o  39411  evl1gprodd  42570  idomnnzgmulnz  42586  abbibw  43124  rexzrexnn0  43250  disjinfi  45640  dvnmptdivc  46384  iblsplitf  46416  vonn0ioo2  47136  vonn0icc2  47138  funressnvmo  47505  ichcircshi  47926  ichreuopeq  47945  paireqne  47983  reuopreuprim  47998  nprmmul3  48001  uspgrsprf1  48635