Theorem equcoms 1756

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 1752	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1757  equtr2  1759  equequ2  1761  ax10o  1763  cbvalv1  1800  cbvexv1  1801  cbvalh  1802  cbvexh  1804  equvini  1807  stdpc7  1819  sbequ12r  1821  sbequ12a  1822  sbequ  1889  sb6rf  1902  cbvalvw  1969  cbvexvw  1970  sb9v  2032  sb6a  2042  mo2n  2108  elequ1  2207  elequ2  2208  cleqh  2332  cbvab  2358  sbralie  2795  reu8  3012  sbcco2  3064  reu8nf  3123  snnex  4568  tfisi  4708  opeliunxp  4804  elrnmpt1  5007  rnxpid  5196  iotaval  5323  elabrex  5929  elabrexg  5930  opabex3d  6313  opabex3  6314  enq0ref  7744  fproddivapf  12310  setindis  16724  bdsetindis  16726