Theorem equcoms 2017

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 2014	. 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 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005

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

This theorem is referenced by:  equtr  2018  equeuclr  2020  spfw  2030  cbvalw  2032  alcomimw  2040  ax8  2112  elequ1  2113  ax9  2120  elequ2  2121  stdpc7  2248  sbequ12r  2250  cbvalv1  2342  cbval  2401  sb9  2522  ax9ALT  2730  sbralieALT  3357  rabrabi  3453  reurab  3710  reu8  3742  sbcco2  3818  reu8nf  3886  notabw  4319  sbcop1  5499  opeliunxp  5756  elrnmpt1  5974  elidinxp  6064  fvn0ssdmfun  7094  elabrex  7262  elabrexg  7263  riotarab  7430  tfisi  7880  tfinds2  7885  opabex3d  7989  opabex3rd  7990  opabex3  7991  xpord2indlem  8171  xpord3inddlem  8178  mpocurryd  8293  boxriin  8979  ixpiunwdom  9628  elirrv  9634  rabssnn0fi  14024  fproddivf  16020  prmodvdslcmf  17081  eqg0subg  19227  1mavmul  22570  ptbasfi  23605  elmptrab  23851  pcoass  25071  iundisj2  25598  dchrisumlema  27547  dchrisumlem2  27549  cusgrfilem2  29489  frgrncvvdeq  30338  frgr2wwlk1  30358  iundisj2f  32610  iundisj2fi  32805  bnj1014  34954  cvmsss2  35259  gonarlem  35379  ax8dfeq  35780  in-ax8  36207  ss-ax8  36208  bj-ssbid1ALT  36648  bj-cbvexw  36659  bj-sb  36670  finxpreclem6  37379  ralssiun  37390  wl-nfs1t  37518  wl-equsb4  37538  wl-euequf  37555  wl-ax11-lem8  37573  matunitlindflem1  37603  poimirlem26  37633  mblfinlem2  37645  sdclem2  37729  axc11-o  38933  evl1gprodd  42099  idomnnzgmulnz  42115  abbibw  42664  rexzrexnn0  42792  disjinfi  45135  dvnmptdivc  45894  iblsplitf  45926  vonn0ioo2  46646  vonn0icc2  46648  funressnvmo  46995  ichcircshi  47379  ichreuopeq  47398  paireqne  47436  reuopreuprim  47451  uspgrsprf1  47991  opeliun2xp  48178