Theorem equcoms 1734

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 1730	. 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 106  ax-gen 1475  ax-ie2 1520  ax-8 1530  ax-17 1552  ax-i9 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1735  equtr2  1737  equequ2  1739  ax10o  1741  cbvalv1  1777  cbvexv1  1778  cbvalh  1779  cbvexh  1781  equvini  1784  stdpc7  1796  sbequ12r  1798  sbequ12a  1799  sbequ  1866  sb6rf  1879  cbvalvw  1946  cbvexvw  1947  sb9v  2009  sb6a  2019  mo2n  2085  elequ1  2184  elequ2  2185  cleqh  2309  cbvab  2333  sbralie  2763  reu8  2979  sbcco2  3031  reu8nf  3090  snnex  4516  tfisi  4656  opeliunxp  4751  elrnmpt1  4951  rnxpid  5139  iotaval  5266  elabrex  5854  elabrexg  5855  opabex3d  6236  opabex3  6237  enq0ref  7588  fproddivapf  12108  setindis  16240  bdsetindis  16242