Theorem equcoms 2015

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 2012	. 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 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774

This theorem is referenced by:  equtr  2016  equeuclr  2018  spfw  2028  cbvalw  2030  alcomiw  2038  ax8  2104  elequ1  2105  ax9  2112  elequ2  2113  stdpc7  2237  sbequ12r  2239  cbvalv1  2331  cbval  2391  sb9  2512  ax9ALT  2720  sbralieALT  3342  rabrabi  3437  reurab  3694  reu8  3726  sbcco2  3802  reu8nf  3869  notabw  4304  ab0OLD  4379  sbcop1  5493  opeliunxp  5748  elrnmpt1  5963  elidinxp  6052  fvn0ssdmfun  7087  elabrex  7256  elabrexg  7257  riotarab  7422  tfisi  7868  tfinds2  7873  opabex3d  7978  opabex3rd  7979  opabex3  7980  xpord2indlem  8160  xpord3inddlem  8167  mpocurryd  8283  boxriin  8968  ixpiunwdom  9629  elirrv  9635  rabssnn0fi  14001  fproddivf  15984  prmodvdslcmf  17044  eqg0subg  19185  1mavmul  22533  ptbasfi  23568  elmptrab  23814  pcoass  25034  iundisj2  25561  dchrisumlema  27509  dchrisumlem2  27511  cusgrfilem2  29385  frgrncvvdeq  30234  frgr2wwlk1  30254  iundisj2f  32501  iundisj2fi  32688  bnj1014  34762  cvmsss2  35054  gonarlem  35174  ax8dfeq  35570  bj-ssbid1ALT  36317  bj-cbvexw  36328  bj-sb  36340  finxpreclem6  37051  ralssiun  37062  wl-nfs1t  37180  wl-equsb4  37200  wl-euequf  37217  wl-ax11-lem8  37235  matunitlindflem1  37265  poimirlem26  37295  mblfinlem2  37307  sdclem2  37391  axc11-o  38597  evl1gprodd  41763  idomnnzgmulnz  41779  abbibw  42269  rexzrexnn0  42398  disjinfi  44736  dvnmptdivc  45496  iblsplitf  45528  vonn0ioo2  46248  vonn0icc2  46250  funressnvmo  46597  ichcircshi  46963  ichreuopeq  46982  paireqne  47020  reuopreuprim  47035  uspgrsprf1  47461  opeliun2xp  47648