Theorem equcoms 2028

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 2025	. 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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788

This theorem is referenced by:  equtr  2029  equeuclr  2031  spfw  2041  cbvalw  2043  alcomimw  2051  ax8  2127  elequ1  2128  ax9  2135  elequ2  2136  stdpc7  2264  sbequ12r  2266  cbvalv1  2351  cbval  2408  sb9  2529  ax9ALT  2736  sbralieALT  3320  rabrabi  3412  reurab  3643  reu8  3675  sbcco2  3751  reu8nf  3810  notabw  4243  sbcop1  5430  opeliunxp  5687  opeliun2xp  5688  elrnmpt1  5908  elidinxp  6002  fvn0ssdmfun  7018  elabrex  7189  elabrexg  7190  riotarab  7358  tfisi  7802  tfinds2  7807  opabex3d  7909  opabex3rd  7910  opabex3  7911  xpord2indlem  8089  xpord3inddlem  8096  mpocurryd  8211  boxriin  8882  ixpiunwdom  9499  elirrvOLD  9507  elirrvOLDOLD  9508  rabssnn0fi  13943  fproddivf  15947  prmodvdslcmf  17013  eqg0subg  19166  1mavmul  22534  ptbasfi  23567  elmptrab  23813  pcoass  25012  iundisj2  25537  dchrisumlema  27472  dchrisumlem2  27474  cusgrfilem2  29545  frgrncvvdeq  30399  frgr2wwlk1  30419  iundisj2f  32681  iundisj2fi  32891  bnj1014  35156  axpowg2  35341  axpowg3  35342  cvmsss2  35515  gonarlem  35635  ax8dfeq  36037  in-ax8  36465  ss-ax8  36466  bj-ssbid1ALT  37018  bj-cbvexw  37030  bj-sb  37043  bj-axseprep  37440  finxpreclem6  37771  ralssiun  37782  wl-nfs1t  37921  wl-equsb4  37941  wl-euequf  37958  matunitlindflem1  37996  poimirlem26  38026  mblfinlem2  38038  sdclem2  38122  axc11-o  39456  evl1gprodd  42615  idomnnzgmulnz  42631  abbibw  43140  rexzrexnn0  43262  disjinfi  45651  dvnmptdivc  46393  iblsplitf  46425  vonn0ioo2  47145  vonn0icc2  47147  funressnvmo  47520  ichcircshi  47941  ichreuopeq  47960  paireqne  47998  reuopreuprim  48013  nprmmul3  48016  uspgrsprf1  48650