Theorem equcoms 2027

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 2024	. 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 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  equtr  2028  equeuclr  2030  spfw  2040  cbvalw  2042  alcomiw  2050  alcomiwOLD  2051  ax8  2117  elequ1  2118  ax9  2125  elequ2  2126  stdpc7  2249  sbequ12r  2251  cbvalv1  2350  cbval  2405  cbvalvOLD  2409  sb9  2538  sbequALT  2573  ax9ALT  2794  sbralie  3418  reu8  3672  sbcco2  3747  reu8nf  3806  sbcop1  5344  opeliunxp  5583  elrnmpt1  5794  elidinxp  5878  fvn0ssdmfun  6819  elabrex  6980  tfisi  7553  tfinds2  7558  opabex3d  7648  opabex3rd  7649  opabex3  7650  mpocurryd  7918  boxriin  8487  ixpiunwdom  9038  elirrv  9044  rabssnn0fi  13349  fproddivf  15333  prmodvdslcmf  16373  1mavmul  21153  ptbasfi  22186  elmptrab  22432  pcoass  23629  iundisj2  24153  dchrisumlema  26072  dchrisumlem2  26074  cusgrfilem2  27246  frgrncvvdeq  28094  frgr2wwlk1  28114  iundisj2f  30353  iundisj2fi  30546  bnj1014  32343  cvmsss2  32634  gonarlem  32754  ax8dfeq  33156  bj-ssbid1ALT  34111  bj-cbvexw  34122  bj-sb  34134  finxpreclem6  34813  ralssiun  34824  wl-nfs1t  34942  wl-equsb4  34958  wl-euequf  34975  wl-ax11-lem8  34989  matunitlindflem1  35053  poimirlem26  35083  mblfinlem2  35095  sdclem2  35180  axc11-o  36247  rexzrexnn0  39745  elabrexg  41675  disjinfi  41820  dvnmptdivc  42580  iblsplitf  42612  vonn0ioo2  43329  vonn0icc2  43331  funressnvmo  43637  ichcircshi  43971  ichreuopeq  43990  paireqne  44028  reuopreuprim  44043  uspgrsprf1  44375  opeliun2xp  44734