Theorem equcoms 2027

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 2024	. 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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  equtr  2028  equeuclr  2030  spfw  2040  cbvalw  2042  alcomimw  2050  ax8  2125  elequ1  2126  ax9  2133  elequ2  2134  stdpc7  2262  sbequ12r  2264  cbvalv1  2349  cbval  2406  sb9  2527  ax9ALT  2735  sbralieALT  3319  rabrabi  3411  reurab  3649  reu8  3681  sbcco2  3757  reu8nf  3816  notabw  4248  sbcop1  5435  opeliunxp  5692  opeliun2xp  5693  elrnmpt1  5909  elidinxp  6003  fvn0ssdmfun  7022  elabrex  7193  elabrexg  7194  riotarab  7362  tfisi  7806  tfinds2  7811  opabex3d  7914  opabex3rd  7915  opabex3  7916  xpord2indlem  8094  xpord3inddlem  8101  mpocurryd  8216  boxriin  8885  ixpiunwdom  9502  elirrvOLD  9510  elirrvOLDOLD  9511  rabssnn0fi  13946  fproddivf  15950  prmodvdslcmf  17016  eqg0subg  19169  1mavmul  22538  ptbasfi  23571  elmptrab  23817  pcoass  25016  iundisj2  25541  dchrisumlema  27476  dchrisumlem2  27478  cusgrfilem2  29550  frgrncvvdeq  30404  frgr2wwlk1  30424  iundisj2f  32686  iundisj2fi  32896  bnj1014  35150  axpowg2  35335  axpowg3  35336  cvmsss2  35509  gonarlem  35629  ax8dfeq  36031  in-ax8  36459  ss-ax8  36460  bj-ssbid1ALT  37012  bj-cbvexw  37024  bj-sb  37037  bj-axseprep  37434  finxpreclem6  37765  ralssiun  37776  wl-nfs1t  37915  wl-equsb4  37935  wl-euequf  37952  matunitlindflem1  37990  poimirlem26  38020  mblfinlem2  38032  sdclem2  38116  axc11-o  39450  evl1gprodd  42609  idomnnzgmulnz  42625  abbibw  43134  rexzrexnn0  43256  disjinfi  45646  dvnmptdivc  46388  iblsplitf  46420  vonn0ioo2  47140  vonn0icc2  47142  funressnvmo  47515  ichcircshi  47936  ichreuopeq  47955  paireqne  47993  reuopreuprim  48008  nprmmul3  48011  uspgrsprf1  48645