New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  equcoms GIF version

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
StepHypRef Expression
1 equcomi 1679 . 2 (y = xx = y)
2 equcoms.1 . 2 (x = yφ)
31, 2syl 15 1 (y = xφ)
 Colors of variables: wff setvar class 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  2471  sbralie  2848  reu8  3032  opeliunxp  4820  addccan2nclem1  6263
 Copyright terms: Public domain W3C validator