Theorem equcoms 1781

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	|- ( x = y -> ph )

Assertion

Ref	Expression
equcoms	|- ( y = x -> ph )

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1779	. 2 |- ( y = x -> x = y )
2		equcoms.1	. 2 |- ( x = y -> ph )
3	1, 2	syl 16	1 |- ( y = x -> ph )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776

This theorem depends on definitions:  df-bi 185  df-ex 1600

This theorem is referenced by:  equtr  1782  stdpc7  1787  equtr2  1788  ax13b  1791  spfw  1792  cbvalw  1794  alcomiw  1797  elequ1  1807  elequ2  1809  19.8a  1843  19.8aOLD  1844  sbequ12r  1979  sbequ12aOLD  1981  cbval  2007  sbequ  2103  sb9  2155  ax13fromc9  2221  axc11-o  2267  euequ1  2274  cleqhOLD  2559  cbvabOLD  2585  reu8  3281  sbcco2  3337  opeliunxp  5041  elrnmpt1  5241  iotaval  5552  fvn0ssdmfun  6007  elabrex  6140  snnex  6591  tfisi  6678  tfinds2  6683  opabex3d  6763  opabex3  6764  mpt2curryd  7000  boxriin  7513  ixpiunwdom  8020  elirrv  8026  rabssnn0fi  12077  imasvscafn  14916  1mavmul  19028  ptbasfi  20060  elmptrab  20306  pcoass  21502  iundisj2  21937  dchrisumlema  23651  dchrisumlem2  23653  cusgrafilem2  24458  frgrancvvdeqlem9  25019  iundisj2f  27427  iundisj2fi  27580  cvmsss2  28697  ax8dfeq  29207  wl-nfs1t  29967  wl-equsb4  29981  wl-ax11-lem8  30008  mblfinlem2  30028  sdclem2  30211  rexzrexnn0  30713  elabrexg  31384  fproddivf  31542  iblsplitf  31723  opeliun2xp  32790  bnj1014  33886  bj-cbvexw  34118  bj-cbvalv  34179  bj-cleqh  34241