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

Theorem eqcoms 2441
Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqcoms.1  |-  ( A  =  B  ->  ph )
Assertion
Ref Expression
eqcoms  |-  ( B  =  A  ->  ph )

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2440 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 195 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-cleq 2431
This theorem is referenced by:  gencbvex  3011  sbceq2a  3193  eqimss2  3404  uneqdifeq  3762  tppreq3  3975  tpprceq3  4008  copsex2t  4573  copsex2g  4574  cnveqb  5288  cnveq0  5289  relcoi1  5361  unixpid  5367  funtpg  5463  tz6.12i  5705  fvcofneq  5846  f1ocnvfv  5980  f1ocnvfvb  5981  cbvfo  5988  ov6g  6223  tfindsg  6466  findsg  6498  suppimacnv  6696  suppss  6714  ectocld  7159  ecoptocl  7182  undifixp  7291  phplem3  7484  card1  8130  pr2ne  8164  prdom2  8165  sornom  8438  indpi  9068  ltlen  9468  eqlei  9476  squeeze0  10227  nn0ind-raph  10734  injresinjlem  11630  hashf1rn  12115  hash1snb  12163  euhash1  12164  hashgt12el  12165  hashgt12el2  12166  hash2prde  12171  hash2prd  12173  hash2pwpr  12174  brfi1uzind  12211  wrdlenfi  12250  lswlgt0cl  12263  wrdeqswrdlsw  12335  wrd2ind  12364  swrdccatin12lem2  12372  swrdccatin12lem3  12373  swrdccat3a  12377  cshweqrep  12447  cshwsexa  12450  2swrd2eqwrdeq  12545  rennim  12720  absmod0  12784  cshwrepswhash1  14121  xpsfrnel2  14495  istos  15197  symgfvne  15884  symgfix2  15912  symgextf1  15917  symgfixelsi  15931  odbezout  16050  cntzcmnss  16316  frgpnabllem1  16342  psgndiflemB  18005  uvcendim  18251  mamufacex  18264  mavmulsolcl  18337  mdetunilem8  18400  bwthOLD  18989  txcn  19174  qtopeu  19264  reeff1o  21887  pntrlog2bndlem5  22805  usgraedg4  23256  usgraidx2vlem2  23261  nbgraf1olem5  23305  nb3graprlem1  23310  cusgrasize2inds  23336  usgrasscusgra  23342  2pthlem2  23446  wlkdvspthlem  23457  fargshiftfv  23472  fargshiftf  23473  usgrcyclnl1  23477  usgrcyclnl2  23478  3v3e3cycl1  23481  constr3trllem2  23488  4cycl4v4e  23503  4cycl4dv4e  23505  vdusgra0nedg  23529  usgravd0nedg  23533  eupatrl  23540  ismgm  23758  rngodm1dm2  23856  rngomndo  23859  rngoueqz  23868  zerdivemp1  23872  cdj1i  25788  br8d  25893  sgn3da  26876  br8  27517  br4  27519  sspred  27584  mblfinlem3  28383  mblfinlem4  28384  itg2addnclem  28396  indexdom  28581  zerdivemp1x  28714  pm13.192  29617  iotavalsb  29640  nvelim  29977  fveqvfvv  29983  funressnfv  29987  afvpcfv0  30005  afv0nbfvbi  30010  fnbrafvb  30013  tz6.12-afv  30032  afvco2  30035  ndmaovg  30043  f0rn0  30094  fzoopth  30166  hashrabsn1  30186  modfsummods  30197  m1dvdsndvds  30200  wwlktovfo  30206  lswn0  30211  ccats1rev  30213  ccatw2s1p1  30222  ccatw2s1p2  30223  wlkn0  30232  usg2wlkeq  30242  usgra2wlkspthlem1  30249  usgra2pth  30254  wwlkn0  30276  wlkiswwlk1  30277  wlkiswwlk2lem3  30280  wlklniswwlkn1  30286  wwlknextbi  30310  wwlknredwwlkn0  30312  wwlkextwrd  30313  wwlkextsur  30316  el2wlkonot  30341  el2spthonot  30342  el2spthonot0  30343  el2wlkonotot0  30344  el2wlkonotot1  30346  usg2spthonot0  30361  clwlkisclwwlklem2a4  30399  clwlkisclwwlklem2a  30400  clwwlkel  30408  clwwlkfo  30412  wwlkext2clwwlk  30418  clwwnisshclwwn  30426  eleclclwwlknlem2  30444  scshwfzeqfzo  30445  erclwwlkneqlen  30451  erclwwlkntr  30454  hashecclwwlkn1  30461  usghashecclwwlk  30462  clwlkfclwwlk  30470  clwlkfoclwwlk  30471  rusgraprop2  30507  wwlkextprop  30516  clwlknclwlkdifs  30531  1to2vfriswmgra  30551  frgrancvvdeqlem3  30578  frgrancvvdeqlem4  30579  frgrancvvdeqlemB  30584  frgrancvvdeqlemC  30585  usgreghash2spotv  30612  extwwlkfablem1  30620  extwwlkfablem2  30624  numclwwlkun  30625  numclwlk1lem2f1  30640  numclwwlk2lem1  30648  numclwlk2lem2f  30649  ztprmneprm  30691  psgnsn  30722  lmod0rng  30730  lincext3  30879  zlmodzxznm  30928  bj-snsetex  32303  bj-snglc  32309  opcon3b  32681  ps-1  32961  3atlem5  32971  4atex  33560
  Copyright terms: Public domain W3C validator