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

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

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2463 . 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 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  gencbvex  3122  sbceq2a  3306  eqimss2  3520  uneqdifeq  3878  tppreq3  4091  tpprceq3  4124  copsex2t  4689  copsex2g  4690  cnveqb  5404  cnveq0  5405  relcoi1  5477  unixpid  5483  funtpg  5579  tz6.12i  5822  fvcofneq  5963  f1ocnvfv  6097  f1ocnvfvb  6098  cbvfo  6105  ov6g  6341  tfindsg  6584  findsg  6616  suppimacnv  6814  suppss  6832  ectocld  7280  ecoptocl  7303  undifixp  7412  phplem3  7605  card1  8252  pr2ne  8286  prdom2  8287  sornom  8560  indpi  9190  ltlen  9590  eqlei  9598  squeeze0  10349  nn0ind-raph  10856  injresinjlem  11758  hashf1rn  12243  hash1snb  12292  euhash1  12293  hashgt12el  12294  hashgt12el2  12295  hash2prde  12300  hash2prd  12302  hash2pwpr  12303  brfi1uzind  12340  wrdlenfi  12379  lswlgt0cl  12392  wrdeqswrdlsw  12464  wrd2ind  12493  swrdccatin12lem2  12501  swrdccatin12lem3  12502  swrdccat3a  12506  cshweqrep  12576  cshwsexa  12579  2swrd2eqwrdeq  12674  rennim  12849  absmod0  12913  cshwrepswhash1  14250  xpsfrnel2  14625  istos  15327  symgfvne  16015  symgfix2  16043  symgextf1  16048  symgfixelsi  16062  psgnsn  16148  odbezout  16183  cntzcmnss  16449  frgpnabllem1  16475  psgndiflemB  18158  uvcendim  18404  mamufacex  18417  mavmulsolcl  18492  mdetunilem8  18560  bwthOLD  19149  txcn  19334  qtopeu  19424  reeff1o  22048  pntrlog2bndlem5  22966  usgraedg4  23477  usgraidx2vlem2  23482  nbgraf1olem5  23526  nb3graprlem1  23531  cusgrasize2inds  23557  usgrasscusgra  23563  2pthlem2  23667  wlkdvspthlem  23678  fargshiftfv  23693  fargshiftf  23694  usgrcyclnl1  23698  usgrcyclnl2  23699  3v3e3cycl1  23702  constr3trllem2  23709  4cycl4v4e  23724  4cycl4dv4e  23726  vdusgra0nedg  23750  usgravd0nedg  23754  eupatrl  23761  ismgm  23979  rngodm1dm2  24077  rngomndo  24080  rngoueqz  24089  zerdivemp1  24093  cdj1i  26009  br8d  26113  sgn3da  27088  br8  27730  br4  27732  sspred  27797  mblfinlem3  28598  mblfinlem4  28599  itg2addnclem  28611  indexdom  28796  zerdivemp1x  28929  pm13.192  29832  iotavalsb  29855  nvelim  30192  fveqvfvv  30198  funressnfv  30202  afvpcfv0  30220  afv0nbfvbi  30225  fnbrafvb  30228  tz6.12-afv  30247  afvco2  30250  ndmaovg  30258  f0rn0  30309  fzoopth  30381  hashrabsn1  30401  modfsummods  30412  m1dvdsndvds  30415  wwlktovfo  30421  lswn0  30426  ccats1rev  30428  ccatw2s1p1  30437  ccatw2s1p2  30438  wlkn0  30447  usg2wlkeq  30457  usgra2wlkspthlem1  30464  usgra2pth  30469  wwlkn0  30491  wlkiswwlk1  30492  wlkiswwlk2lem3  30495  wlklniswwlkn1  30501  wwlknextbi  30525  wwlknredwwlkn0  30527  wwlkextwrd  30528  wwlkextsur  30531  el2wlkonot  30556  el2spthonot  30557  el2spthonot0  30558  el2wlkonotot0  30559  el2wlkonotot1  30561  usg2spthonot0  30576  clwlkisclwwlklem2a4  30614  clwlkisclwwlklem2a  30615  clwwlkel  30623  clwwlkfo  30627  wwlkext2clwwlk  30633  clwwnisshclwwn  30641  eleclclwwlknlem2  30659  scshwfzeqfzo  30660  erclwwlkneqlen  30666  erclwwlkntr  30669  hashecclwwlkn1  30676  usghashecclwwlk  30677  clwlkfclwwlk  30685  clwlkfoclwwlk  30686  rusgraprop2  30722  wwlkextprop  30731  clwlknclwlkdifs  30746  1to2vfriswmgra  30766  frgrancvvdeqlem3  30793  frgrancvvdeqlem4  30794  frgrancvvdeqlemB  30799  frgrancvvdeqlemC  30800  usgreghash2spotv  30827  extwwlkfablem1  30835  extwwlkfablem2  30839  numclwwlkun  30840  numclwlk1lem2f1  30855  numclwwlk2lem1  30863  numclwlk2lem2f  30864  ztprmneprm  30907  lmod0rng  30947  lincext3  31142  zlmodzxznm  31191  pm2mpfo  31321  cpscmat  31348  chmaidscmat  31354  chfacfscmulgsum  31366  chfacfpmmulgsum  31370  bj-snsetex  32808  bj-snglc  32814  opcon3b  33199  ps-1  33479  3atlem5  33489  4atex  34078
  Copyright terms: Public domain W3C validator