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  3318  rabrabi  3416  reurab  3663  reu8  3695  sbcco2  3771  reu8nf  3831  notabw  4266  sbcop1  5435  opeliunxp  5690  opeliun2xp  5691  elrnmpt1  5906  elidinxp  5999  fvn0ssdmfun  7012  elabrex  7182  elabrexg  7183  riotarab  7352  tfisi  7799  tfinds2  7804  opabex3d  7907  opabex3rd  7908  opabex3  7909  xpord2indlem  8087  xpord3inddlem  8094  mpocurryd  8209  boxriin  8874  ixpiunwdom  9501  elirrv  9508  elirrvOLD  9509  rabssnn0fi  13911  fproddivf  15912  prmodvdslcmf  16977  eqg0subg  19093  1mavmul  22451  ptbasfi  23484  elmptrab  23730  pcoass  24940  iundisj2  25466  dchrisumlema  27415  dchrisumlem2  27417  cusgrfilem2  29420  frgrncvvdeq  30271  frgr2wwlk1  30291  iundisj2f  32552  iundisj2fi  32753  bnj1014  34927  cvmsss2  35246  gonarlem  35366  ax8dfeq  35771  in-ax8  36197  ss-ax8  36198  bj-ssbid1ALT  36638  bj-cbvexw  36649  bj-sb  36660  finxpreclem6  37369  ralssiun  37380  wl-nfs1t  37510  wl-equsb4  37530  wl-euequf  37547  wl-ax11-lem8  37565  matunitlindflem1  37595  poimirlem26  37625  mblfinlem2  37637  sdclem2  37721  axc11-o  38929  evl1gprodd  42090  idomnnzgmulnz  42106  abbibw  42650  rexzrexnn0  42777  disjinfi  45170  dvnmptdivc  45920  iblsplitf  45952  vonn0ioo2  46672  vonn0icc2  46674  funressnvmo  47030  ichcircshi  47439  ichreuopeq  47458  paireqne  47496  reuopreuprim  47511  uspgrsprf1  48132