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  2152  elequ1  2153  ax9  2160  elequ2  2161  stdpc7  2289  sbequ12r  2291  cbvalv1  2376  cbval  2433  sb9  2554  ax9ALT  2761  sbralieALT  3346  rabrabi  3438  reurab  3667  reu8  3699  sbcco2  3774  reu8nf  3833  notabw  4269  sbcop1  5475  opeliunxp  5733  opeliun2xp  5734  elrnmpt1  5955  elidinxp  6051  fvn0ssdmfun  7076  elabrex  7247  elabrexg  7248  riotarab  7422  tfisi  7864  tfinds2  7869  opabex3d  7971  opabex3rd  7972  opabex3  7973  xpord2indlem  8152  xpord3inddlem  8159  mpocurryd  8274  boxriin  8947  ixpiunwdom  9562  elirrvOLD  9570  elirrvOLDOLD  9571  rabssnn0fi  14042  fproddivf  16067  prmodvdslcmf  17132  eqg0subg  19298  1mavmul  22742  ptbasfi  23775  elmptrab  24021  pcoass  25220  iundisj2  25745  dchrisumlema  27689  dchrisumlem2  27691  cusgrfilem2  29843  frgrncvvdeq  30697  frgr2wwlk1  30717  iundisj2f  32972  iundisj2fi  33179  bnj1014  35381  axpowg2  35584  axpowg3  35585  cvmsss2  35787  gonarlem  35907  ax8dfeq  36309  in-ax8  36777  ss-ax8  36778  bj-ssbid1ALT  37328  bj-cbvexw  37340  bj-sb  37353  bj-axseprep  37752  finxpreclem6  38083  ralssiun  38094  wl-nfs1t  38233  wl-equsb4  38253  wl-euequf  38270  matunitlindflem1  38308  poimirlem26  38338  mblfinlem2  38350  sdclem2  38434  axc11-o  39766  evl1gprodd  42925  idomnnzgmulnz  42941  abbibw  43450  rexzrexnn0  43572  disjinfi  45951  dvnmptdivc  46693  iblsplitf  46725  vonn0ioo2  47445  vonn0icc2  47447  funressnvmo  47823  ichcircshi  48244  ichreuopeq  48263  paireqne  48301  reuopreuprim  48316  nprmmul3  48319  uspgrsprf1  48953