Theorem equcoms 2053

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 2050	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 18	1 ⊢ (𝑦 = 𝑥 → 𝜑)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  equtr  2054  equeuclr  2056  spfw  2066  cbvalw  2068  alcomimw  2076  ax8  2151  elequ1  2152  ax9  2159  elequ2  2160  stdpc7  2286  sbequ12r  2288  cbvalv1  2371  cbval  2428  sb9  2549  ax9ALT  2756  sbralieALT  3340  rabrabi  3431  reurab  3659  reu8  3691  sbcco2  3766  reu8nf  3824  notabw  4259  sbcop1  5458  opeliunxp  5718  opeliun2xp  5719  elrnmpt1  5942  elidinxp  6038  fvn0ssdmfun  7066  elabrex  7238  elabrexg  7239  riotarab  7411  tfisi  7859  tfinds2  7864  opabex3d  7966  opabex3rd  7967  opabex3  7968  xpord2indlem  8148  xpord3inddlem  8155  mpocurryd  8270  boxriin  8952  ixpiunwdom  9568  elirrvOLD  9576  elirrvOLDOLD  9577  rabssnn0fi  14109  fproddivf  16134  prmodvdslcmf  17205  eqg0subg  19391  1mavmul  22843  matunitlindflem1  22974  ptbasfi  23880  elmptrab  24126  pcoass  25325  iundisj2  25850  dchrisumlema  27797  dchrisumlem2  27799  cusgrfilem2  30019  frgrncvvdeq  30892  frgr2wwlk1  30912  iundisj2f  33166  iundisj2fi  33371  bnj1014  35574  axpowg2  35788  axpowg3  35789  cvmsss2  36008  gonarlem  36128  ax8dfeq  36530  in-ax8  36983  ss-ax8  36984  bj-ssbid1ALT  37534  bj-cbvexw  37546  bj-sb  37559  bj-axseprep  37958  finxpreclem6  38287  ralssiun  38298  wl-nfs1t  38437  wl-equsb4  38457  wl-euequf  38474  poimirlem26  38532  mblfinlem2  38544  sdclem2  38644  axc11-o  39976  evl1gprodd  43135  idomnnzgmulnz  43151  abbibw  43642  rexzrexnn0  43764  disjinfi  46150  dvnmptdivc  46892  iblsplitf  46924  vonn0ioo2  47644  vonn0icc2  47646  funressnvmo  48059  ichcircshi  48480  ichreuopeq  48499  paireqne  48537  reuopreuprim  48552  nprmmul3  48555  uspgrsprf1  49189