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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  equtr  2020  equeuclr  2022  spfw  2032  cbvalw  2034  alcomimw  2042  ax8  2114  elequ1  2115  ax9  2122  elequ2  2123  stdpc7  2251  sbequ12r  2253  cbvalv1  2347  cbval  2406  sb9  2527  ax9ALT  2735  sbralieALT  3367  rabrabi  3463  reurab  3723  reu8  3755  sbcco2  3831  reu8nf  3899  notabw  4332  ab0OLD  4403  sbcop1  5508  opeliunxp  5767  elrnmpt1  5983  elidinxp  6073  fvn0ssdmfun  7108  elabrex  7279  elabrexg  7280  riotarab  7447  tfisi  7896  tfinds2  7901  opabex3d  8006  opabex3rd  8007  opabex3  8008  xpord2indlem  8188  xpord3inddlem  8195  mpocurryd  8310  boxriin  8998  ixpiunwdom  9659  elirrv  9665  rabssnn0fi  14037  fproddivf  16035  prmodvdslcmf  17094  eqg0subg  19236  1mavmul  22575  ptbasfi  23610  elmptrab  23856  pcoass  25076  iundisj2  25603  dchrisumlema  27550  dchrisumlem2  27552  cusgrfilem2  29492  frgrncvvdeq  30341  frgr2wwlk1  30361  iundisj2f  32612  iundisj2fi  32802  bnj1014  34937  cvmsss2  35242  gonarlem  35362  ax8dfeq  35762  in-ax8  36190  ss-ax8  36191  bj-ssbid1ALT  36631  bj-cbvexw  36642  bj-sb  36653  finxpreclem6  37362  ralssiun  37373  wl-nfs1t  37491  wl-equsb4  37511  wl-euequf  37528  wl-ax11-lem8  37546  matunitlindflem1  37576  poimirlem26  37606  mblfinlem2  37618  sdclem2  37702  axc11-o  38907  evl1gprodd  42074  idomnnzgmulnz  42090  abbibw  42632  rexzrexnn0  42760  disjinfi  45099  dvnmptdivc  45859  iblsplitf  45891  vonn0ioo2  46611  vonn0icc2  46613  funressnvmo  46960  ichcircshi  47328  ichreuopeq  47347  paireqne  47385  reuopreuprim  47400  uspgrsprf1  47870  opeliun2xp  48057