Theorem equcoms 2055

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 2052	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 18	1 ⊢ (𝑦 = 𝑥 → 𝜑)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  equtr  2056  equeuclr  2058  spfw  2068  cbvalw  2070  alcomimw  2078  ax8  2153  elequ1  2154  ax9  2161  elequ2  2162  stdpc7  2289  sbequ12r  2291  cbvalv1  2374  cbval  2430  sb9  2551  ax9ALT  2758  sbralieALT  3343  rabrabi  3434  reurab  3662  reu8  3694  sbcco2  3769  reu8nf  3828  notabw  4261  sbcop1  5462  opeliunxp  5722  opeliun2xp  5723  elrnmpt1  5949  elidinxp  6048  fvn0ssdmfun  7098  elabrex  7269  elabrexg  7270  riotarab  7442  tfisi  7894  tfinds2  7899  opabex3d  8001  opabex3rd  8002  opabex3  8003  xpord2indlem  8191  xpord3inddlem  8198  mpocurryd  8314  boxriin  8996  ixpiunwdom  9611  elirrvOLD  9619  elirrvOLDOLD  9620  rabssnn0fi  14156  fproddivf  16183  prmodvdslcmf  17254  eqg0subg  19440  1mavmul  22893  matunitlindflem1  23024  ptbasfi  23930  elmptrab  24176  pcoass  25375  iundisj2  25900  dchrisumlema  27845  dchrisumlem2  27847  cusgrfilem2  30067  frgrncvvdeq  30940  frgr2wwlk1  30960  iundisj2f  33256  iundisj2fi  33459  bnj1014  35661  axpowg2  35915  axpowg3  35916  cvmsss2  36206  gonarlem  36326  ax8dfeq  36738  in-ax8  37191  ss-ax8  37192  bj-ssbid1ALT  37742  bj-cbvexw  37754  bj-sb  37767  bj-axseprep  38181  finxpreclem6  38511  ralssiun  38522  wl-nfs1t  38661  wl-equsb4  38681  wl-euequf  38698  poimirlem26  38756  mblfinlem2  38768  sdclem2  38868  axc11-o  40200  evl1gprodd  43359  idomnnzgmulnz  43375  abbibw  43881  rexzrexnn0  44004  disjinfi  46412  dvnmptdivc  47153  iblsplitf  47185  vonn0ioo2  47905  vonn0icc2  47907  funressnvmo  48320  ichcircshi  48741  ichreuopeq  48760  paireqne  48798  reuopreuprim  48813  nprmmul3  48816  uspgrsprf1  49450