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  3325  rabrabi  3420  reurab  3661  reu8  3693  sbcco2  3769  reu8nf  3829  notabw  4267  sbcop1  5444  opeliunxp  5699  opeliun2xp  5700  elrnmpt1  5917  elidinxp  6011  fvn0ssdmfun  7028  elabrex  7198  elabrexg  7199  riotarab  7367  tfisi  7811  tfinds2  7816  opabex3d  7919  opabex3rd  7920  opabex3  7921  xpord2indlem  8099  xpord3inddlem  8106  mpocurryd  8221  boxriin  8890  ixpiunwdom  9507  elirrv  9514  elirrvOLD  9515  rabssnn0fi  13921  fproddivf  15922  prmodvdslcmf  16987  eqg0subg  19137  1mavmul  22504  ptbasfi  23537  elmptrab  23783  pcoass  24992  iundisj2  25518  dchrisumlema  27467  dchrisumlem2  27469  cusgrfilem2  29542  frgrncvvdeq  30396  frgr2wwlk1  30416  iundisj2f  32676  iundisj2fi  32887  bnj1014  35136  cvmsss2  35487  gonarlem  35607  ax8dfeq  36009  in-ax8  36437  ss-ax8  36438  bj-ssbid1ALT  36904  bj-cbvexw  36915  bj-sb  36926  bj-axseprep  37316  finxpreclem6  37645  ralssiun  37656  wl-nfs1t  37786  wl-equsb4  37806  wl-euequf  37823  matunitlindflem1  37861  poimirlem26  37891  mblfinlem2  37903  sdclem2  37987  axc11-o  39321  evl1gprodd  42481  idomnnzgmulnz  42497  abbibw  43029  rexzrexnn0  43155  disjinfi  45545  dvnmptdivc  46290  iblsplitf  46322  vonn0ioo2  47042  vonn0icc2  47044  funressnvmo  47399  ichcircshi  47808  ichreuopeq  47827  paireqne  47865  reuopreuprim  47880  uspgrsprf1  48501