Theorem equcoms 2050

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 2047	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 18	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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  equtr  2051  equeuclr  2053  spfw  2063  cbvalw  2065  alcomimw  2073  ax8  2149  elequ1  2150  ax9  2157  elequ2  2158  stdpc7  2286  sbequ12r  2288  cbvalv1  2373  cbval  2430  sb9  2551  ax9ALT  2758  sbralieALT  3343  rabrabi  3435  reurab  3665  reu8  3697  sbcco2  3772  reu8nf  3831  notabw  4267  sbcop1  5472  opeliunxp  5730  opeliun2xp  5731  elrnmpt1  5952  elidinxp  6048  fvn0ssdmfun  7071  elabrex  7242  elabrexg  7243  riotarab  7411  tfisi  7856  tfinds2  7861  opabex3d  7963  opabex3rd  7964  opabex3  7965  xpord2indlem  8144  xpord3inddlem  8151  mpocurryd  8266  boxriin  8939  ixpiunwdom  9553  elirrvOLD  9561  elirrvOLDOLD  9562  rabssnn0fi  14024  fproddivf  16043  prmodvdslcmf  17108  eqg0subg  19268  1mavmul  22686  ptbasfi  23719  elmptrab  23965  pcoass  25164  iundisj2  25689  dchrisumlema  27630  dchrisumlem2  27632  cusgrfilem2  29784  frgrncvvdeq  30638  frgr2wwlk1  30658  iundisj2f  32913  iundisj2fi  33120  bnj1014  35327  axpowg2  35538  axpowg3  35539  cvmsss2  35744  gonarlem  35864  ax8dfeq  36266  in-ax8  36714  ss-ax8  36715  bj-ssbid1ALT  37265  bj-cbvexw  37277  bj-sb  37290  bj-axseprep  37689  finxpreclem6  38020  ralssiun  38031  wl-nfs1t  38170  wl-equsb4  38190  wl-euequf  38207  matunitlindflem1  38245  poimirlem26  38275  mblfinlem2  38287  sdclem2  38371  axc11-o  39703  evl1gprodd  42862  idomnnzgmulnz  42878  abbibw  43389  rexzrexnn0  43511  disjinfi  45890  dvnmptdivc  46632  iblsplitf  46664  vonn0ioo2  47384  vonn0icc2  47386  funressnvmo  47759  ichcircshi  48180  ichreuopeq  48199  paireqne  48237  reuopreuprim  48252  nprmmul3  48255  uspgrsprf1  48889