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 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781

This theorem is referenced by:  equtr  2028  equeuclr  2030  spfw  2040  cbvalw  2042  alcomiw  2050  alcomiwOLD  2051  sbequOLD  2092  ax8  2120  elequ1  2121  ax9  2128  elequ2  2129  stdpc7  2252  sbequ12r  2254  sbequvvOLD  2335  cbvalv1  2361  cbval  2416  cbvalvOLD  2420  sb9  2561  sbequALT  2597  ax9ALT  2817  sbralie  3471  reu8  3724  sbcco2  3799  reu8nf  3860  sbcop1  5379  opeliunxp  5619  elrnmpt1  5830  elidinxp  5911  fvn0ssdmfun  6842  elabrex  7002  tfisi  7573  tfinds2  7578  opabex3d  7666  opabex3rd  7667  opabex3  7668  mpocurryd  7935  boxriin  8504  ixpiunwdom  9055  elirrv  9060  rabssnn0fi  13355  fproddivf  15341  prmodvdslcmf  16383  1mavmul  21157  ptbasfi  22189  elmptrab  22435  pcoass  23628  iundisj2  24150  dchrisumlema  26064  dchrisumlem2  26066  cusgrfilem2  27238  frgrncvvdeq  28088  frgr2wwlk1  28108  iundisj2f  30340  iundisj2fi  30520  bnj1014  32233  cvmsss2  32521  gonarlem  32641  ax8dfeq  33043  bj-ssbid1ALT  33998  bj-cbvexw  34009  bj-sb  34021  finxpreclem6  34680  ralssiun  34691  wl-nfs1t  34792  wl-equsb4  34808  wl-euequf  34825  wl-ax11-lem8  34839  matunitlindflem1  34903  poimirlem26  34933  mblfinlem2  34945  sdclem2  35032  axc11-o  36102  rexzrexnn0  39421  elabrexg  41323  disjinfi  41474  dvnmptdivc  42243  iblsplitf  42275  vonn0ioo2  42992  vonn0icc2  42994  funressnvmo  43300  ichcircshi  43632  ichreuopeq  43655  paireqne  43693  reuopreuprim  43708  uspgrsprf1  44042  opeliun2xp  44401