Theorem equcoms 2090

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 2087	. 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 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842

This theorem is referenced by:  equtr  2091  equeuclr  2093  stdpc7  2099  spfw  2104  spfwOLD  2105  cbvalw  2107  alcomiw  2110  ax8  2133  elequ1  2134  ax9  2140  elequ2  2141  sbequ12r  2247  cbvalv1  2308  cbval  2404  cbvalv  2406  sbequ  2501  sb9  2551  reu8  3531  sbcco2  3588  reu8nf  3645  opeliunxp  5315  elrnmpt1  5517  fvn0ssdmfun  6501  elabrex  6652  snnexOLD  7120  tfisi  7211  tfinds2  7216  opabex3d  7298  opabex3  7299  mpt2curryd  7552  boxriin  8104  ixpiunwdom  8649  elirrv  8654  rabssnn0fi  12950  fproddivf  14888  prmodvdslcmf  15924  imasvscafn  16370  1mavmul  20527  ptbasfi  21557  elmptrab  21803  pcoass  22995  iundisj2  23488  dchrisumlema  25347  dchrisumlem2  25349  cusgrfilem2  26533  frgrncvvdeq  27434  frgr2wwlk1  27454  iundisj2f  29681  iundisj2fi  29836  bnj1014  31308  cvmsss2  31534  ax8dfeq  31980  bj-ssbid1ALT  32925  bj-cbvexw  32941  bj-sb  32954  bj-cleljustab  33124  bj-ax9-2  33168  finxpreclem6  33515  wl-nfs1t  33606  wl-equsb4  33620  wl-euequ1f  33638  wl-ax11-lem8  33651  wl-ax8clv1  33660  wl-clelv2-just  33661  matunitlindflem1  33687  poimirlem26  33717  mblfinlem2  33729  sdclem2  33820  axc11-o  34709  rexzrexnn0  37839  elabrexg  39674  disjinfi  39848  dvnmptdivc  40625  iblsplitf  40658  vonn0ioo2  41379  vonn0icc2  41381  uspgrsprf1  42234  opeliun2xp  42590