Theorem equcoms 2043

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 2040	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 18	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 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803

This theorem is referenced by:  equtr  2044  equeuclr  2046  spfw  2056  cbvalw  2058  alcomimw  2066  ax8  2151  elequ1  2152  ax9  2159  elequ2  2160  stdpc7  2288  sbequ12r  2290  cbvalv1  2375  cbval  2432  sb9  2553  ax9ALT  2760  sbralieALT  3344  rabrabi  3436  reurab  3667  reu8  3699  sbcco2  3774  reu8nf  3833  notabw  4268  sbcop1  5461  opeliunxp  5719  opeliun2xp  5720  elrnmpt1  5941  elidinxp  6037  fvn0ssdmfun  7059  elabrex  7230  elabrexg  7231  riotarab  7399  tfisi  7843  tfinds2  7848  opabex3d  7950  opabex3rd  7951  opabex3  7952  xpord2indlem  8131  xpord3inddlem  8138  mpocurryd  8253  boxriin  8926  ixpiunwdom  9540  elirrvOLD  9548  elirrvOLDOLD  9549  rabssnn0fi  14013  fproddivf  16031  prmodvdslcmf  17097  eqg0subg  19258  1mavmul  22666  ptbasfi  23699  elmptrab  23945  pcoass  25144  iundisj2  25669  dchrisumlema  27610  dchrisumlem2  27612  cusgrfilem2  29715  frgrncvvdeq  30569  frgr2wwlk1  30589  iundisj2f  32845  iundisj2fi  33054  bnj1014  35266  axpowg2  35455  axpowg3  35456  cvmsss2  35637  gonarlem  35757  ax8dfeq  36159  in-ax8  36597  ss-ax8  36598  bj-ssbid1ALT  37149  bj-cbvexw  37161  bj-sb  37174  bj-axseprep  37571  finxpreclem6  37902  ralssiun  37913  wl-nfs1t  38052  wl-equsb4  38072  wl-euequf  38089  matunitlindflem1  38127  poimirlem26  38157  mblfinlem2  38169  sdclem2  38253  axc11-o  39587  evl1gprodd  42746  idomnnzgmulnz  42762  abbibw  43271  rexzrexnn0  43393  disjinfi  45768  dvnmptdivc  46510  iblsplitf  46542  vonn0ioo2  47262  vonn0icc2  47264  funressnvmo  47637  ichcircshi  48058  ichreuopeq  48077  paireqne  48115  reuopreuprim  48130  nprmmul3  48133  uspgrsprf1  48767