Theorem equcoms 2039

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 2036	. 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 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  equtr  2040  equeuclr  2042  spfw  2052  cbvalw  2054  alcomimw  2062  ax8  2147  elequ1  2148  ax9  2155  elequ2  2156  stdpc7  2284  sbequ12r  2286  cbvalv1  2371  cbval  2428  sb9  2549  ax9ALT  2756  sbralieALT  3340  rabrabi  3432  reurab  3663  reu8  3695  sbcco2  3771  reu8nf  3830  notabw  4265  sbcop1  5455  opeliunxp  5712  opeliun2xp  5713  elrnmpt1  5934  elidinxp  6030  fvn0ssdmfun  7051  elabrex  7222  elabrexg  7223  riotarab  7391  tfisi  7835  tfinds2  7840  opabex3d  7942  opabex3rd  7943  opabex3  7944  xpord2indlem  8122  xpord3inddlem  8129  mpocurryd  8244  boxriin  8918  ixpiunwdom  9535  elirrvOLD  9543  elirrvOLDOLD  9544  rabssnn0fi  13996  fproddivf  16000  prmodvdslcmf  17066  eqg0subg  19220  1mavmul  22588  ptbasfi  23621  elmptrab  23867  pcoass  25066  iundisj2  25591  dchrisumlema  27529  dchrisumlem2  27531  cusgrfilem2  29603  frgrncvvdeq  30457  frgr2wwlk1  30477  iundisj2f  32739  iundisj2fi  32949  bnj1014  35220  axpowg2  35407  axpowg3  35408  cvmsss2  35588  gonarlem  35708  ax8dfeq  36110  in-ax8  36548  ss-ax8  36549  bj-ssbid1ALT  37101  bj-cbvexw  37113  bj-sb  37126  bj-axseprep  37523  finxpreclem6  37854  ralssiun  37865  wl-nfs1t  38004  wl-equsb4  38024  wl-euequf  38041  matunitlindflem1  38079  poimirlem26  38109  mblfinlem2  38121  sdclem2  38205  axc11-o  39539  evl1gprodd  42698  idomnnzgmulnz  42714  abbibw  43223  rexzrexnn0  43345  disjinfi  45734  dvnmptdivc  46476  iblsplitf  46508  vonn0ioo2  47228  vonn0icc2  47230  funressnvmo  47603  ichcircshi  48024  ichreuopeq  48043  paireqne  48081  reuopreuprim  48096  nprmmul3  48099  uspgrsprf1  48733