Theorem equcoms 2053

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 2050	. 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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  equtr  2054  equeuclr  2056  spfw  2066  cbvalw  2068  alcomimw  2076  ax8  2151  elequ1  2152  ax9  2159  elequ2  2160  stdpc7  2287  sbequ12r  2289  cbvalv1  2372  cbval  2429  sb9  2550  ax9ALT  2757  sbralieALT  3341  rabrabi  3433  reurab  3662  reu8  3694  sbcco2  3769  reu8nf  3827  notabw  4262  sbcop1  5468  opeliunxp  5726  opeliun2xp  5727  elrnmpt1  5948  elidinxp  6044  fvn0ssdmfun  7071  elabrex  7243  elabrexg  7244  riotarab  7416  tfisi  7859  tfinds2  7864  opabex3d  7966  opabex3rd  7967  opabex3  7968  xpord2indlem  8149  xpord3inddlem  8156  mpocurryd  8271  boxriin  8951  ixpiunwdom  9566  elirrvOLD  9574  elirrvOLDOLD  9575  rabssnn0fi  14054  fproddivf  16080  prmodvdslcmf  17145  eqg0subg  19330  1mavmul  22776  matunitlindflem1  22907  ptbasfi  23813  elmptrab  24059  pcoass  25258  iundisj2  25783  dchrisumlema  27732  dchrisumlem2  27734  cusgrfilem2  29924  frgrncvvdeq  30797  frgr2wwlk1  30817  iundisj2f  33071  iundisj2fi  33276  bnj1014  35478  axpowg2  35681  axpowg3  35682  cvmsss2  35861  gonarlem  35981  ax8dfeq  36383  in-ax8  36852  ss-ax8  36853  bj-ssbid1ALT  37403  bj-cbvexw  37415  bj-sb  37428  bj-axseprep  37827  finxpreclem6  38158  ralssiun  38169  wl-nfs1t  38308  wl-equsb4  38328  wl-euequf  38345  poimirlem26  38403  mblfinlem2  38415  sdclem2  38500  axc11-o  39832  evl1gprodd  42991  idomnnzgmulnz  43007  abbibw  43531  rexzrexnn0  43653  disjinfi  46032  dvnmptdivc  46774  iblsplitf  46806  vonn0ioo2  47526  vonn0icc2  47528  funressnvmo  47941  ichcircshi  48362  ichreuopeq  48381  paireqne  48419  reuopreuprim  48434  nprmmul3  48437  uspgrsprf1  49071