Theorem equcoms 1944

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 1941	. 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 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932

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

This theorem is referenced by:  equtr  1945  equeuclr  1947  equtr2OLD  1953  stdpc7  1955  equvinvOLD  1959  spfw  1962  spfwOLD  1963  cbvalw  1965  alcomiw  1968  ax8  1993  elequ1  1994  ax9  2000  elequ2  2001  19.8aOLD  2050  sbequ12r  2109  cbvalv1  2174  cbval  2270  cbvalv  2272  sbequ  2375  sb9  2425  reu8  3384  sbcco2  3441  opeliunxp  5131  elrnmpt1  5334  fvn0ssdmfun  6306  elabrex  6455  snnex  6917  tfisi  7005  tfinds2  7010  opabex3d  7091  opabex3  7092  mpt2curryd  7340  boxriin  7894  ixpiunwdom  8440  elirrv  8448  rabssnn0fi  12725  fproddivf  14643  prmodvdslcmf  15675  imasvscafn  16118  1mavmul  20273  ptbasfi  21294  elmptrab  21540  pcoass  22732  iundisj2  23224  dchrisumlema  25077  dchrisumlem2  25079  cusgrfilem2  26239  frgrncvvdeq  27038  iundisj2f  29245  iundisj2fi  29394  bnj1014  30735  cvmsss2  30961  ax8dfeq  31402  bj-ssbid1ALT  32287  bj-cbvexw  32303  bj-sb  32316  bj-cleljustab  32489  bj-ax9-2  32535  finxpreclem6  32862  wl-nfs1t  32953  wl-equsb4  32967  wl-euequ1f  32985  wl-ax11-lem8  32998  wl-ax8clv1  33007  wl-clelv2-just  33008  matunitlindflem1  33034  poimirlem26  33064  mblfinlem2  33076  sdclem2  33167  axc11-o  33713  rexzrexnn0  36845  elabrexg  38686  disjinfi  38851  dvnmptdivc  39456  iblsplitf  39490  vonn0ioo2  40208  vonn0icc2  40210  uspgrsprf1  41040  opeliun2xp  41396