Theorem equcoms 2067

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 2064	. 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 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824

This theorem is referenced by:  equtr  2068  equeuclr  2070  stdpc7  2076  spfw  2083  cbvalw  2085  alcomiw  2088  alcomiwOLD  2089  ax8  2113  elequ1  2114  ax9  2120  elequ2  2121  sbequ12r  2230  sbequvv  2288  cbvalv1  2312  cbval  2368  cbvalv  2370  sbequ  2452  sb9  2503  rabrabi  3397  reu8  3614  sbcco2  3676  reu8nf  3733  opeliunxp  5418  elrnmpt1  5622  elidinxp  5707  fvn0ssdmfun  6616  elabrex  6775  tfisi  7338  tfinds2  7343  opabex3d  7425  opabex3  7426  mpt2curryd  7679  boxriin  8238  ixpiunwdom  8787  elirrv  8792  rabssnn0fi  13108  fproddivf  15124  prmodvdslcmf  16159  1mavmul  20763  ptbasfi  21797  elmptrab  22043  pcoass  23235  iundisj2  23757  dchrisumlema  25633  dchrisumlem2  25635  cusgrfilem2  26808  frgrncvvdeq  27721  frgr2wwlk1  27741  iundisj2f  29970  iundisj2fi  30124  bnj1014  31633  cvmsss2  31859  ax8dfeq  32296  bj-ssbid1ALT  33242  bj-cbvexw  33257  bj-sb  33270  bj-cleljustab  33426  bj-ax9-2  33466  finxpreclem6  33831  wl-nfs1t  33921  wl-equsb4  33936  wl-euequf  33953  wl-ax11-lem8  33966  wl-ax8clv1  34008  wl-clelv2-just  34009  matunitlindflem1  34036  poimirlem26  34066  mblfinlem2  34078  sdclem2  34167  axc11-o  35110  rexzrexnn0  38338  elabrexg  40149  disjinfi  40313  dvnmptdivc  41091  iblsplitf  41123  vonn0ioo2  41841  vonn0icc2  41843  funressnvmo  42119  funressnvmoOLD  42120  paireqne  42460  uspgrsprf1  42780  opeliun2xp  43136