MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqcoms Structured version   Visualization version   GIF version

Theorem eqcoms 2659
Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)
Hypothesis
Ref Expression
eqcoms.1 (𝐴 = 𝐵𝜑)
Assertion
Ref Expression
eqcoms (𝐵 = 𝐴𝜑)

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2658 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 207 1 (𝐵 = 𝐴𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  gencbvex  3281  sbceq2a  3480  eqimss2  3691  uneqdifeq  4090  uneqdifeqOLD  4091  tppreq3  4326  ifpprsnss  4331  tpprceq3  4367  elpr2elpr  4429  prproe  4466  copsex2t  4986  copsex2g  4987  relopabi  5278  cnveqb  5625  cnveq0  5626  unixpid  5708  funtpgOLD  5981  f0rn0  6128  f1ssf1  6206  tz6.12i  6252  fveqdmss  6394  fvcofneq  6407  funopsn  6453  f1ocnvfv  6574  f1ocnvfvb  6575  cbvfo  6584  riotaeqimp  6674  ov6g  6840  tfindsg  7102  findsg  7135  suppimacnv  7351  suppss  7370  ectocld  7857  ecoptocl  7880  undifixp  7986  phplem3  8182  f1dmvrnfibi  8291  f1vrnfibi  8292  card1  8832  pr2ne  8866  prdom2  8867  sornom  9137  indpi  9767  ltlen  10176  eqlei  10185  squeeze0  10964  nn0ind-raph  11515  injresinjlem  12628  modmuladd  12752  modmuladdnn0  12754  hashf1rn  13181  hashrabsn1  13201  hash1snb  13245  hashgt12el  13248  hashgt12el2  13249  hashfzp1  13256  hash2prde  13290  hash2pwpr  13296  fi1uzind  13317  brfi1indALT  13320  lswlgt0cl  13389  wrd2ind  13523  reuccats1lem  13525  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccat3a  13540  cshweqrep  13613  cshwsexa  13616  scshwfzeqfzo  13618  cshimadifsn  13621  cshimadifsn0  13622  2swrd2eqwrdeq  13742  wwlktovfo  13747  rennim  14023  absmod0  14087  modfsummods  14569  mod2eq1n2dvds  15118  m1expe  15138  m1expo  15139  m1exp1  15140  nn0o1gt2  15144  flodddiv4  15184  cncongr1  15428  m1dvdsndvds  15550  cshwrepswhash1  15856  xpsfrnel2  16272  initoeu2lem1  16711  istos  17082  symgfvne  17854  symgfix2  17882  symgextf1  17887  symgfixelsi  17901  psgnsn  17986  odbezout  18021  cntzcmnss  18292  frgpnabllem1  18322  ringinvnzdiv  18639  psgndiflemB  19994  uvcendim  20234  mamufacex  20243  smatvscl  20378  mavmulsolcl  20405  mdetunilem8  20473  pm2mpfo  20667  chpscmat  20695  chmaidscmat  20701  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  txcn  21477  qtopeu  21567  reeff1o  24246  relogbcxpb  24570  zabsle1  25066  2lgslem1c  25163  2lgsoddprmlem3  25184  pntrlog2bndlem5  25315  upgrpredgv  26079  usgredg2vlem2  26163  ushgredgedg  26166  ushgredgedgloop  26168  uhgrspan1  26240  nb3grprlem1  26326  uvtxnbgrb  26352  cplgruvtxbOLD  26367  cusgrsize2inds  26405  1egrvtxdg0  26463  uspgrloopvtxel  26468  finsumvtxdg2size  26502  rusgrpropnb  26535  ifpsnprss  26574  upgrwlkvtxedg  26597  uspgr2wlkeq  26598  wlkp1lem5  26630  wlkp1  26634  usgr2pth  26716  uspgrn2crct  26756  iswwlksnon  26802  wlkiswwlks1  26821  wlkiswwlks2lem3  26825  wwlksnextbi  26857  wwlksnredwwlkn0  26859  wwlksnextwrd  26860  wwlksnextsur  26863  wwlksnextprop  26875  wspn0  26889  umgr2adedgwlkonALT  26912  umgr2adedgspth  26913  umgr2wlkon  26915  elwwlks2ons3  26920  elwwlks2ons3OLD  26921  elwwlks2on  26925  clwwlknclwwlkdifsOLD  26947  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwwlkel  27009  clwwlkfo  27013  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  eleclclwwlknlem2  27026  erclwwlkntr  27035  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfclwwlk  27049  clwlksfoclwwlk  27050  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  0wlkonlem1  27096  upgr1wlkdlem1  27123  1pthon2v  27131  upgr3v3e3cycl  27158  uhgr3cyclexlem  27159  upgr4cycl4dv4e  27163  eupth2lem3lem3  27208  eupth2lem3lem4  27209  1to2vfriswmgr  27259  frgrncvvdeqlem6  27284  frgrncvvdeqlem8  27286  frgrncvvdeqlem9  27287  frgrwopreglem2  27293  2clwwlk2clwwlk  27338  extwwlkfab  27342  numclwlk1lem2f1  27347  numclwwlkovh  27353  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  cdj1i  29420  brabgaf  29546  br8d  29548  sgn3da  30731  mthmb  31604  br8  31772  br4  31774  bj-snsetex  33076  bj-snglc  33082  poimirlem20  33559  poimirlem26  33565  poimirlem27  33566  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem  33591  indexdom  33659  ismgmOLD  33779  rngodm1dm2  33861  rngomndo  33864  rngoueqz  33869  zerdivemp1x  33876  opcon3b  34801  ps-1  35081  3atlem5  35091  4atex  35680  pm13.192  38928  iotavalsb  38951  fourierdlem32  40674  fourierdlem49  40690  fourierdlem64  40705  nvelim  41521  fveqvfvv  41525  funressnfv  41529  afvpcfv0  41547  afv0nbfvbi  41552  fnbrafvb  41555  tz6.12-afv  41574  afvco2  41577  ndmaovg  41585  elprneb  41620  fzoopth  41662  iccpartiltu  41683  fargshiftfv  41700  fargshiftf  41701  lswn0  41705  pfxsuffeqwrdeq  41731  pfxccatin12lem2  41749  fmtnorec2lem  41779  2pwp1prm  41828  lighneallem2  41848  lighneallem3  41849  proththd  41856  nn0o1gt2ALTV  41930  evenltle  41951  sbgoldbwt  41990  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  prsprel  42062  uspgropssxp  42077  lmod0rng  42193  lidldomn1  42246  zlidlring  42253  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  ztprmneprm  42450  lincext3  42570  zlmodzxznm  42611  suppdm  42625  elfzolborelfzop1  42634  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator