Theorem equcoms 1701

Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
equcoms.1	⊢ (𝑥 = 𝑦 → 𝜑)

Assertion

Ref	Expression
equcoms	⊢ (𝑦 = 𝑥 → 𝜑)

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1697	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 14	1 ⊢ (𝑦 = 𝑥 → 𝜑)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equtr  1702  equtr2  1704  equequ2  1706  ax10o  1708  cbvalv1  1744  cbvexv1  1745  cbvalh  1746  cbvexh  1748  equvini  1751  stdpc7  1763  sbequ12r  1765  sbequ12a  1766  sbequ  1833  sb6rf  1846  cbvalvw  1912  cbvexvw  1913  sb9v  1971  sb6a  1981  mo2n  2047  elequ1  2145  elequ2  2146  cleqh  2270  cbvab  2294  sbralie  2714  reu8  2926  sbcco2  2977  snnex  4433  tfisi  4571  opeliunxp  4666  elrnmpt1  4862  rnxpid  5045  iotaval  5171  elabrex  5737  opabex3d  6100  opabex3  6101  enq0ref  7395  fproddivapf  11594  setindis  14002  bdsetindis  14004