Theorem equcoms 1947

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 1944	. 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 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  equtr  1948  equeuclr  1950  equtr2OLD  1956  stdpc7  1958  equvinvOLD  1962  spfw  1965  spfwOLD  1966  cbvalw  1968  alcomiw  1971  ax8  1996  elequ1  1997  ax9  2003  elequ2  2004  sbequ12r  2112  cbvalv1  2175  cbval  2271  cbvalv  2273  sbequ  2376  sb9  2426  reu8  3402  sbcco2  3459  reu8nf  3516  opeliunxp  5170  elrnmpt1  5374  fvn0ssdmfun  6350  elabrex  6501  snnexOLD  6967  tfisi  7058  tfinds2  7063  opabex3d  7145  opabex3  7146  mpt2curryd  7395  boxriin  7950  ixpiunwdom  8496  elirrv  8504  rabssnn0fi  12785  fproddivf  14718  prmodvdslcmf  15751  imasvscafn  16197  1mavmul  20354  ptbasfi  21384  elmptrab  21630  pcoass  22824  iundisj2  23317  dchrisumlema  25177  dchrisumlem2  25179  cusgrfilem2  26352  frgrncvvdeq  27173  frgr2wwlk1  27193  iundisj2f  29403  iundisj2fi  29556  bnj1014  31030  cvmsss2  31256  ax8dfeq  31704  bj-ssbid1ALT  32648  bj-cbvexw  32664  bj-sb  32677  bj-cleljustab  32847  bj-ax9-2  32891  finxpreclem6  33233  wl-nfs1t  33324  wl-equsb4  33338  wl-euequ1f  33356  wl-ax11-lem8  33369  wl-ax8clv1  33378  wl-clelv2-just  33379  matunitlindflem1  33405  poimirlem26  33435  mblfinlem2  33447  sdclem2  33538  axc11-o  34236  rexzrexnn0  37368  elabrexg  39206  disjinfi  39380  dvnmptdivc  40153  iblsplitf  40186  vonn0ioo2  40904  vonn0icc2  40906  uspgrsprf1  41755  opeliun2xp  42111