Theorem equcoms 2018

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 2015	. 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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006

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

This theorem is referenced by:  equtr  2019  equeuclr  2021  spfw  2031  cbvalw  2033  alcomimw  2041  ax8  2113  elequ1  2114  ax9  2121  elequ2  2122  stdpc7  2249  sbequ12r  2251  cbvalv1  2341  cbval  2401  sb9  2522  ax9ALT  2729  sbralieALT  3336  rabrabi  3433  reurab  3682  reu8  3714  sbcco2  3790  reu8nf  3850  notabw  4286  sbcop1  5460  opeliunxp  5718  opeliun2xp  5719  elrnmpt1  5937  elidinxp  6028  fvn0ssdmfun  7060  elabrex  7230  elabrexg  7231  riotarab  7398  tfisi  7848  tfinds2  7853  opabex3d  7958  opabex3rd  7959  opabex3  7960  xpord2indlem  8140  xpord3inddlem  8147  mpocurryd  8262  boxriin  8948  ixpiunwdom  9596  elirrv  9602  rabssnn0fi  13993  fproddivf  15990  prmodvdslcmf  17052  eqg0subg  19164  1mavmul  22471  ptbasfi  23504  elmptrab  23750  pcoass  24960  iundisj2  25487  dchrisumlema  27435  dchrisumlem2  27437  cusgrfilem2  29368  frgrncvvdeq  30222  frgr2wwlk1  30242  iundisj2f  32504  iundisj2fi  32708  bnj1014  34913  cvmsss2  35217  gonarlem  35337  ax8dfeq  35737  in-ax8  36163  ss-ax8  36164  bj-ssbid1ALT  36604  bj-cbvexw  36615  bj-sb  36626  finxpreclem6  37335  ralssiun  37346  wl-nfs1t  37476  wl-equsb4  37496  wl-euequf  37513  wl-ax11-lem8  37531  matunitlindflem1  37561  poimirlem26  37591  mblfinlem2  37603  sdclem2  37687  axc11-o  38890  evl1gprodd  42052  idomnnzgmulnz  42068  abbibw  42625  rexzrexnn0  42752  disjinfi  45143  dvnmptdivc  45897  iblsplitf  45929  vonn0ioo2  46649  vonn0icc2  46651  funressnvmo  47002  ichcircshi  47386  ichreuopeq  47405  paireqne  47443  reuopreuprim  47458  uspgrsprf1  48008