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  2342  cbval  2402  sb9  2523  ax9ALT  2730  sbralieALT  3338  rabrabi  3435  reurab  3684  reu8  3716  sbcco2  3792  reu8nf  3852  notabw  4288  sbcop1  5463  opeliunxp  5721  opeliun2xp  5722  elrnmpt1  5940  elidinxp  6031  fvn0ssdmfun  7064  elabrex  7234  elabrexg  7235  riotarab  7404  tfisi  7854  tfinds2  7859  opabex3d  7964  opabex3rd  7965  opabex3  7966  xpord2indlem  8146  xpord3inddlem  8153  mpocurryd  8268  boxriin  8954  ixpiunwdom  9604  elirrv  9610  rabssnn0fi  14004  fproddivf  16003  prmodvdslcmf  17067  eqg0subg  19179  1mavmul  22486  ptbasfi  23519  elmptrab  23765  pcoass  24975  iundisj2  25502  dchrisumlema  27451  dchrisumlem2  27453  cusgrfilem2  29436  frgrncvvdeq  30290  frgr2wwlk1  30310  iundisj2f  32571  iundisj2fi  32774  bnj1014  34992  cvmsss2  35296  gonarlem  35416  ax8dfeq  35816  in-ax8  36242  ss-ax8  36243  bj-ssbid1ALT  36683  bj-cbvexw  36694  bj-sb  36705  finxpreclem6  37414  ralssiun  37425  wl-nfs1t  37555  wl-equsb4  37575  wl-euequf  37592  wl-ax11-lem8  37610  matunitlindflem1  37640  poimirlem26  37670  mblfinlem2  37682  sdclem2  37766  axc11-o  38969  evl1gprodd  42130  idomnnzgmulnz  42146  abbibw  42700  rexzrexnn0  42827  disjinfi  45216  dvnmptdivc  45967  iblsplitf  45999  vonn0ioo2  46719  vonn0icc2  46721  funressnvmo  47074  ichcircshi  47468  ichreuopeq  47487  paireqne  47525  reuopreuprim  47540  uspgrsprf1  48122