Theorem equcoms 2052

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 2049	. 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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

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

This theorem is used by:  equtr  2053  equeuclr  2055  spfw  2065  cbvalw  2067  alcomimw  2075  ax8  2150  elequ1  2151  ax9  2158  elequ2  2159  stdpc7  2285  sbequ12r  2287  cbvalv1  2370  cbval  2427  sb9  2548  ax9ALT  2755  sbralieALT  3339  rabrabi  3430  reurab  3658  reu8  3690  sbcco2  3765  reu8nf  3823  notabw  4258  sbcop1  5457  opeliunxp  5717  opeliun2xp  5718  elrnmpt1  5941  elidinxp  6035  fvn0ssdmfun  7074  elabrex  7246  elabrexg  7247  riotarab  7419  tfisi  7870  tfinds2  7875  opabex3d  7977  opabex3rd  7978  opabex3  7979  xpord2indlem  8166  xpord3inddlem  8173  mpocurryd  8289  boxriin  8971  ixpiunwdom  9587  elirrvOLD  9595  elirrvOLDOLD  9596  rabssnn0fi  14132  fproddivf  16159  prmodvdslcmf  17230  eqg0subg  19416  1mavmul  22868  matunitlindflem1  22999  ptbasfi  23905  elmptrab  24151  pcoass  25350  iundisj2  25875  dchrisumlema  27820  dchrisumlem2  27822  cusgrfilem2  30042  frgrncvvdeq  30915  frgr2wwlk1  30935  iundisj2f  33231  iundisj2fi  33435  bnj1014  35637  axpowg2  35871  axpowg3  35872  cvmsss2  36125  gonarlem  36245  ax8dfeq  36652  in-ax8  37105  ss-ax8  37106  bj-ssbid1ALT  37656  bj-cbvexw  37668  bj-sb  37681  bj-axseprep  38082  finxpreclem6  38412  ralssiun  38423  wl-nfs1t  38562  wl-equsb4  38582  wl-euequf  38599  poimirlem26  38657  mblfinlem2  38669  sdclem2  38769  axc11-o  40101  evl1gprodd  43260  idomnnzgmulnz  43276  abbibw  43781  rexzrexnn0  43904  disjinfi  46300  dvnmptdivc  47041  iblsplitf  47073  vonn0ioo2  47793  vonn0icc2  47795  funressnvmo  48208  ichcircshi  48629  ichreuopeq  48648  paireqne  48686  reuopreuprim  48701  nprmmul3  48704  uspgrsprf1  49338