Theorem equcoms 2027

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 2024	. 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 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015

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

This theorem is referenced by:  equtr  2028  equeuclr  2030  spfw  2040  cbvalw  2042  alcomiw  2050  alcomiwOLD  2051  ax8  2116  elequ1  2117  ax9  2124  elequ2  2125  stdpc7  2247  sbequ12r  2249  cbvalv1  2342  cbval  2400  sb9  2525  ax9ALT  2735  sbralie  3404  rabrabi  3426  reu8  3672  sbcco2  3747  reu8nf  3815  notabw  4243  ab0OLD  4315  sbcop1  5406  opeliunxp  5655  elrnmpt1  5866  elidinxp  5950  fvn0ssdmfun  6949  elabrex  7113  tfisi  7699  tfinds2  7704  opabex3d  7801  opabex3rd  7802  opabex3  7803  mpocurryd  8076  boxriin  8711  ixpiunwdom  9327  elirrv  9333  rabssnn0fi  13704  fproddivf  15695  prmodvdslcmf  16746  1mavmul  21695  ptbasfi  22730  elmptrab  22976  pcoass  24185  iundisj2  24711  dchrisumlema  26634  dchrisumlem2  26636  cusgrfilem2  27821  frgrncvvdeq  28669  frgr2wwlk1  28689  iundisj2f  30925  iundisj2fi  31114  bnj1014  32937  cvmsss2  33232  gonarlem  33352  riotarab  33669  reurab  33670  ax8dfeq  33770  xpord2ind  33790  xpord3ind  33796  bj-ssbid1ALT  34842  bj-cbvexw  34853  bj-sb  34865  finxpreclem6  35563  ralssiun  35574  wl-nfs1t  35692  wl-equsb4  35708  wl-euequf  35725  wl-ax11-lem8  35739  matunitlindflem1  35769  poimirlem26  35799  mblfinlem2  35811  sdclem2  35896  axc11-o  36961  rexzrexnn0  40623  elabrexg  42559  disjinfi  42701  dvnmptdivc  43450  iblsplitf  43482  vonn0ioo2  44199  vonn0icc2  44201  funressnvmo  44507  ichcircshi  44875  ichreuopeq  44894  paireqne  44932  reuopreuprim  44947  uspgrsprf1  45278  opeliun2xp  45637