MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equcoms Structured version   Unicode version

Theorem equcoms 1800
Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
equcoms.1  |-  ( x  =  y  ->  ph )
Assertion
Ref Expression
equcoms  |-  ( y  =  x  ->  ph )

Proof of Theorem equcoms
StepHypRef Expression
1 equcomi 1798 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 16 1  |-  ( y  =  x  ->  ph )
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 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795
This theorem depends on definitions:  df-bi 185  df-ex 1618
This theorem is referenced by:  equtr  1801  stdpc7  1806  equtr2  1807  ax13b  1810  spfw  1811  cbvalw  1813  alcomiw  1816  elequ1  1826  elequ2  1828  19.8a  1862  19.8aOLD  1863  sbequ12r  1998  sbequ12aOLD  2000  cbval  2026  sbequ  2119  sb9  2171  ax13fromc9  2237  axc11-o  2283  euequ1  2290  cleqhOLD  2570  cbvabOLD  2596  reu8  3292  sbcco2  3348  opeliunxp  5040  elrnmpt1  5240  iotaval  5545  fvn0ssdmfun  5998  elabrex  6130  snnex  6579  tfisi  6666  tfinds2  6671  opabex3d  6751  opabex3  6752  mpt2curryd  6990  boxriin  7504  ixpiunwdom  8009  elirrv  8015  rabssnn0fi  12080  imasvscafn  15029  1mavmul  19220  ptbasfi  20251  elmptrab  20497  pcoass  21693  iundisj2  22128  dchrisumlema  23874  dchrisumlem2  23876  cusgrafilem2  24685  frgrancvvdeqlem9  25246  iundisj2f  27663  iundisj2fi  27839  cvmsss2  28986  ax8dfeq  29474  wl-nfs1t  30234  wl-equsb4  30248  wl-ax11-lem8  30275  mblfinlem2  30295  sdclem2  30478  rexzrexnn0  30980  elabrexg  31673  fproddivf  31830  iblsplitf  32011  opeliun2xp  33195  bnj1014  34438  bj-cbvexw  34655  bj-cbvalv  34716  bj-cleqh  34778
  Copyright terms: Public domain W3C validator