Theorem equcoms 1681

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	⊢ (x = y → φ)

Assertion

Ref	Expression
equcoms	⊢ (y = x → φ)

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1679	. 2 ⊢ (y = x → x = y)
2		equcoms.1	. 2 ⊢ (x = y → φ)
3	1, 2	syl 15	1 ⊢ (y = x → φ)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  equtr  1682  equtr2  1688  ax12b  1689  ax12bOLD  1690  spfw  1691  spw  1694  cbvalw  1701  cbvalvw  1702  alcomiw  1704  elequ1  1713  elequ2  1715  stdpc7  1917  sbequ12r  1920  sbequ12a  1921  ax12olem1  1927  ax12  1935  ax10o  1952  cbval  1984  equvini  1987  sbequ  2060  sb6rf  2091  sb6a  2116  ax12from12o  2156  ax10o-o  2203  mo  2226  cleqh  2450  cbvab  2472  sbralie  2849  reu8  3033  opeliunxp  4821  addccan2nclem1  6264