Theorem equcoms 2024

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 2021	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  equtr  2025  equeuclr  2027  spfw  2037  cbvalw  2039  alcomiw  2047  alcomiwOLD  2048  ax8  2113  elequ1  2114  ax9  2121  elequ2  2122  stdpc7  2244  sbequ12r  2246  cbvalv1  2339  cbval  2399  sb9  2524  ax9ALT  2734  sbralie  3407  rabrabi  3428  reu8  3669  sbcco2  3744  reu8nf  3811  notabw  4238  ab0OLD  4310  sbcop1  5403  opeliunxp  5655  elrnmpt1  5870  elidinxp  5954  fvn0ssdmfun  6961  elabrex  7125  tfisi  7714  tfinds2  7719  opabex3d  7817  opabex3rd  7818  opabex3  7819  mpocurryd  8094  boxriin  8737  ixpiunwdom  9358  elirrv  9364  rabssnn0fi  13715  fproddivf  15706  prmodvdslcmf  16757  1mavmul  21706  ptbasfi  22741  elmptrab  22987  pcoass  24196  iundisj2  24722  dchrisumlema  26645  dchrisumlem2  26647  cusgrfilem2  27832  frgrncvvdeq  28682  frgr2wwlk1  28702  iundisj2f  30938  iundisj2fi  31127  bnj1014  32950  cvmsss2  33245  gonarlem  33365  riotarab  33682  reurab  33683  ax8dfeq  33783  xpord2ind  33803  xpord3ind  33809  bj-ssbid1ALT  34855  bj-cbvexw  34866  bj-sb  34878  finxpreclem6  35576  ralssiun  35587  wl-nfs1t  35705  wl-equsb4  35721  wl-euequf  35738  wl-ax11-lem8  35752  matunitlindflem1  35782  poimirlem26  35812  mblfinlem2  35824  sdclem2  35909  axc11-o  36972  rexzrexnn0  40633  elabrexg  42596  disjinfi  42738  dvnmptdivc  43486  iblsplitf  43518  vonn0ioo2  44235  vonn0icc2  44237  funressnvmo  44550  ichcircshi  44917  ichreuopeq  44936  paireqne  44974  reuopreuprim  44989  uspgrsprf1  45320  opeliun2xp  45679