Theorem equcoms 2019

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 2016	. 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 2007

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

This theorem is referenced by:  equtr  2020  equeuclr  2022  spfw  2032  cbvalw  2034  alcomimw  2042  ax8  2114  elequ1  2115  ax9  2122  elequ2  2123  stdpc7  2250  sbequ12r  2252  cbvalv1  2343  cbval  2403  sb9  2524  ax9ALT  2732  sbralieALT  3359  rabrabi  3456  reurab  3707  reu8  3739  sbcco2  3815  reu8nf  3877  notabw  4313  sbcop1  5493  opeliunxp  5752  opeliun2xp  5753  elrnmpt1  5971  elidinxp  6062  fvn0ssdmfun  7094  elabrex  7262  elabrexg  7263  riotarab  7430  tfisi  7880  tfinds2  7885  opabex3d  7990  opabex3rd  7991  opabex3  7992  xpord2indlem  8172  xpord3inddlem  8179  mpocurryd  8294  boxriin  8980  ixpiunwdom  9630  elirrv  9636  rabssnn0fi  14027  fproddivf  16023  prmodvdslcmf  17085  eqg0subg  19214  1mavmul  22554  ptbasfi  23589  elmptrab  23835  pcoass  25057  iundisj2  25584  dchrisumlema  27532  dchrisumlem2  27534  cusgrfilem2  29474  frgrncvvdeq  30328  frgr2wwlk1  30348  iundisj2f  32603  iundisj2fi  32799  bnj1014  34975  cvmsss2  35279  gonarlem  35399  ax8dfeq  35799  in-ax8  36225  ss-ax8  36226  bj-ssbid1ALT  36666  bj-cbvexw  36677  bj-sb  36688  finxpreclem6  37397  ralssiun  37408  wl-nfs1t  37538  wl-equsb4  37558  wl-euequf  37575  wl-ax11-lem8  37593  matunitlindflem1  37623  poimirlem26  37653  mblfinlem2  37665  sdclem2  37749  axc11-o  38952  evl1gprodd  42118  idomnnzgmulnz  42134  abbibw  42687  rexzrexnn0  42815  disjinfi  45197  dvnmptdivc  45953  iblsplitf  45985  vonn0ioo2  46705  vonn0icc2  46707  funressnvmo  47057  ichcircshi  47441  ichreuopeq  47460  paireqne  47498  reuopreuprim  47513  uspgrsprf1  48063