Theorem equcoms 2020

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 2017	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  equtr  2021  equeuclr  2023  spfw  2033  cbvalw  2035  alcomimw  2043  ax8  2115  elequ1  2116  ax9  2123  elequ2  2124  stdpc7  2251  sbequ12r  2253  cbvalv1  2339  cbval  2396  sb9  2517  ax9ALT  2724  sbralieALT  3327  rabrabi  3425  reurab  3672  reu8  3704  sbcco2  3780  reu8nf  3840  notabw  4276  sbcop1  5448  opeliunxp  5705  opeliun2xp  5706  elrnmpt1  5924  elidinxp  6015  fvn0ssdmfun  7046  elabrex  7216  elabrexg  7217  riotarab  7386  tfisi  7835  tfinds2  7840  opabex3d  7944  opabex3rd  7945  opabex3  7946  xpord2indlem  8126  xpord3inddlem  8133  mpocurryd  8248  boxriin  8913  ixpiunwdom  9543  elirrv  9549  rabssnn0fi  13951  fproddivf  15953  prmodvdslcmf  17018  eqg0subg  19128  1mavmul  22435  ptbasfi  23468  elmptrab  23714  pcoass  24924  iundisj2  25450  dchrisumlema  27399  dchrisumlem2  27401  cusgrfilem2  29384  frgrncvvdeq  30238  frgr2wwlk1  30258  iundisj2f  32519  iundisj2fi  32720  bnj1014  34951  cvmsss2  35261  gonarlem  35381  ax8dfeq  35786  in-ax8  36212  ss-ax8  36213  bj-ssbid1ALT  36653  bj-cbvexw  36664  bj-sb  36675  finxpreclem6  37384  ralssiun  37395  wl-nfs1t  37525  wl-equsb4  37545  wl-euequf  37562  wl-ax11-lem8  37580  matunitlindflem1  37610  poimirlem26  37640  mblfinlem2  37652  sdclem2  37736  axc11-o  38944  evl1gprodd  42105  idomnnzgmulnz  42121  abbibw  42665  rexzrexnn0  42792  disjinfi  45186  dvnmptdivc  45936  iblsplitf  45968  vonn0ioo2  46688  vonn0icc2  46690  funressnvmo  47046  ichcircshi  47455  ichreuopeq  47474  paireqne  47512  reuopreuprim  47527  uspgrsprf1  48135