Theorem equcoms 2020

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 2017	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  equtr  2021  equeuclr  2023  spfw  2033  cbvalw  2035  alcomimw  2043  ax8  2115  elequ1  2116  ax9  2123  elequ2  2124  stdpc7  2251  sbequ12r  2253  cbvalv1  2339  cbval  2397  sb9  2518  ax9ALT  2725  sbralieALT  3329  rabrabi  3428  reurab  3675  reu8  3707  sbcco2  3783  reu8nf  3843  notabw  4279  sbcop1  5451  opeliunxp  5708  opeliun2xp  5709  elrnmpt1  5927  elidinxp  6018  fvn0ssdmfun  7049  elabrex  7219  elabrexg  7220  riotarab  7389  tfisi  7838  tfinds2  7843  opabex3d  7947  opabex3rd  7948  opabex3  7949  xpord2indlem  8129  xpord3inddlem  8136  mpocurryd  8251  boxriin  8916  ixpiunwdom  9550  elirrv  9556  rabssnn0fi  13958  fproddivf  15960  prmodvdslcmf  17025  eqg0subg  19135  1mavmul  22442  ptbasfi  23475  elmptrab  23721  pcoass  24931  iundisj2  25457  dchrisumlema  27406  dchrisumlem2  27408  cusgrfilem2  29391  frgrncvvdeq  30245  frgr2wwlk1  30265  iundisj2f  32526  iundisj2fi  32727  bnj1014  34958  cvmsss2  35268  gonarlem  35388  ax8dfeq  35793  in-ax8  36219  ss-ax8  36220  bj-ssbid1ALT  36660  bj-cbvexw  36671  bj-sb  36682  finxpreclem6  37391  ralssiun  37402  wl-nfs1t  37532  wl-equsb4  37552  wl-euequf  37569  wl-ax11-lem8  37587  matunitlindflem1  37617  poimirlem26  37647  mblfinlem2  37659  sdclem2  37743  axc11-o  38951  evl1gprodd  42112  idomnnzgmulnz  42128  abbibw  42672  rexzrexnn0  42799  disjinfi  45193  dvnmptdivc  45943  iblsplitf  45975  vonn0ioo2  46695  vonn0icc2  46697  funressnvmo  47050  ichcircshi  47459  ichreuopeq  47478  paireqne  47516  reuopreuprim  47531  uspgrsprf1  48139