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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  equtr  2025  equeuclr  2027  spfw  2037  cbvalw  2039  alcomiw  2047  alcomiwOLD  2048  ax8  2114  elequ1  2115  ax9  2122  elequ2  2123  stdpc7  2246  sbequ12r  2248  cbvalv1  2340  cbval  2398  sb9  2523  ax9ALT  2733  sbralie  3395  rabrabi  3417  reu8  3663  sbcco2  3738  reu8nf  3806  notabw  4234  ab0OLD  4306  sbcop1  5396  opeliunxp  5645  elrnmpt1  5856  elidinxp  5940  fvn0ssdmfun  6934  elabrex  7098  tfisi  7680  tfinds2  7685  opabex3d  7781  opabex3rd  7782  opabex3  7783  mpocurryd  8056  boxriin  8686  ixpiunwdom  9279  elirrv  9285  rabssnn0fi  13634  fproddivf  15625  prmodvdslcmf  16676  1mavmul  21605  ptbasfi  22640  elmptrab  22886  pcoass  24093  iundisj2  24618  dchrisumlema  26541  dchrisumlem2  26543  cusgrfilem2  27726  frgrncvvdeq  28574  frgr2wwlk1  28594  iundisj2f  30830  iundisj2fi  31020  bnj1014  32841  cvmsss2  33136  gonarlem  33256  riotarab  33575  reurab  33576  ax8dfeq  33680  xpord2ind  33721  xpord3ind  33727  bj-ssbid1ALT  34773  bj-cbvexw  34784  bj-sb  34796  finxpreclem6  35494  ralssiun  35505  wl-nfs1t  35623  wl-equsb4  35639  wl-euequf  35656  wl-ax11-lem8  35670  matunitlindflem1  35700  poimirlem26  35730  mblfinlem2  35742  sdclem2  35827  axc11-o  36892  rexzrexnn0  40542  elabrexg  42478  disjinfi  42620  dvnmptdivc  43369  iblsplitf  43401  vonn0ioo2  44118  vonn0icc2  44120  funressnvmo  44426  ichcircshi  44794  ichreuopeq  44813  paireqne  44851  reuopreuprim  44866  uspgrsprf1  45197  opeliun2xp  45556