Theorem equcoms 2105

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 2102	. 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 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853

This theorem is referenced by:  equtr  2106  equeuclr  2108  stdpc7  2114  spfw  2121  spfwOLD  2122  cbvalw  2124  alcomiw  2127  alcomiwOLD  2128  ax8  2151  elequ1  2152  ax9  2158  elequ2  2159  sbequ12r  2268  cbvalv1  2336  cbval  2432  cbvalv  2434  sbequ  2523  sb9  2573  rabrabi  3350  reu8  3555  sbcco2  3612  reu8nf  3666  opeliunxp  5311  elrnmpt1  5513  fvn0ssdmfun  6494  elabrex  6645  snnexOLD  7115  tfisi  7206  tfinds2  7211  opabex3d  7293  opabex3  7294  mpt2curryd  7548  boxriin  8105  ixpiunwdom  8653  elirrv  8658  rabssnn0fi  12994  fproddivf  14925  prmodvdslcmf  15959  1mavmul  20573  ptbasfi  21606  elmptrab  21852  pcoass  23044  iundisj2  23538  dchrisumlema  25399  dchrisumlem2  25401  cusgrfilem2  26588  frgrncvvdeq  27492  frgr2wwlk1  27512  iundisj2f  29742  iundisj2fi  29897  bnj1014  31369  cvmsss2  31595  ax8dfeq  32041  bj-ssbid1ALT  32986  bj-cbvexw  33002  bj-sb  33015  bj-cleljustab  33182  bj-ax9-2  33221  finxpreclem6  33571  wl-nfs1t  33660  wl-equsb4  33674  wl-euequ1f  33691  wl-ax11-lem8  33704  wl-ax8clv1  33712  wl-clelv2-just  33713  matunitlindflem1  33739  poimirlem26  33769  mblfinlem2  33781  sdclem2  33871  axc11-o  34760  rexzrexnn0  37895  elabrexg  39729  disjinfi  39901  dvnmptdivc  40672  iblsplitf  40704  vonn0ioo2  41425  vonn0icc2  41427  uspgrsprf1  42284  opeliun2xp  42640