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

Theorem eqcoms 2436
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 2435 . 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 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-cleq 2426
This theorem is referenced by:  gencbvex  3005  sbceq2a  3186  eqimss2  3397  uneqdifeq  3755  tppreq3  3968  tpprceq3  4001  copsex2t  4566  copsex2g  4567  cnveqb  5281  cnveq0  5282  relcoi1  5354  unixpid  5360  funtpg  5456  tz6.12i  5698  fvcofneq  5839  f1ocnvfv  5972  f1ocnvfvb  5973  cbvfo  5980  ov6g  6217  tfindsg  6460  findsg  6492  suppimacnv  6690  suppss  6708  ectocld  7155  ecoptocl  7178  undifixp  7287  phplem3  7480  card1  8126  pr2ne  8160  prdom2  8161  sornom  8434  indpi  9063  ltlen  9463  eqlei  9471  squeeze0  10222  nn0ind-raph  10729  injresinjlem  11621  hashf1rn  12106  hash1snb  12154  euhash1  12155  hashgt12el  12156  hashgt12el2  12157  hash2prde  12162  hash2prd  12164  hash2pwpr  12165  brfi1uzind  12202  wrdlenfi  12241  lswlgt0cl  12254  wrdeqswrdlsw  12326  wrd2ind  12355  swrdccatin12lem2  12363  swrdccatin12lem3  12364  swrdccat3a  12368  cshweqrep  12438  cshwsexa  12441  2swrd2eqwrdeq  12536  rennim  12711  absmod0  12775  cshwrepswhash1  14111  xpsfrnel2  14485  istos  15187  symgfvne  15872  symgfix2  15900  symgextf1  15905  symgfixelsi  15919  odbezout  16038  cntzcmnss  16304  frgpnabllem1  16330  psgndiflemB  17871  uvcendim  18117  mamufacex  18130  mavmulsolcl  18203  mdetunilem8  18266  bwthOLD  18855  txcn  19040  qtopeu  19130  reeff1o  21796  pntrlog2bndlem5  22714  usgraedg4  23127  usgraidx2vlem2  23132  nbgraf1olem5  23176  nb3graprlem1  23181  cusgrasize2inds  23207  usgrasscusgra  23213  2pthlem2  23317  wlkdvspthlem  23328  fargshiftfv  23343  fargshiftf  23344  usgrcyclnl1  23348  usgrcyclnl2  23349  3v3e3cycl1  23352  constr3trllem2  23359  4cycl4v4e  23374  4cycl4dv4e  23376  vdusgra0nedg  23400  usgravd0nedg  23404  eupatrl  23411  ismgm  23629  rngodm1dm2  23727  rngomndo  23730  rngoueqz  23739  zerdivemp1  23743  cdj1i  25659  br8d  25765  sgn3da  26771  br8  27412  br4  27414  sspred  27479  mblfinlem3  28271  mblfinlem4  28272  itg2addnclem  28284  indexdom  28469  zerdivemp1x  28602  pm13.192  29506  iotavalsb  29529  nvelim  29867  fveqvfvv  29873  funressnfv  29877  afvpcfv0  29895  afv0nbfvbi  29900  fnbrafvb  29903  tz6.12-afv  29922  afvco2  29925  ndmaovg  29933  f0rn0  29984  fzoopth  30056  hashrabsn1  30076  modfsummods  30087  m1dvdsndvds  30090  wwlktovfo  30096  lswn0  30101  ccats1rev  30103  ccatw2s1p1  30112  ccatw2s1p2  30113  wlkn0  30122  usg2wlkeq  30132  usgra2wlkspthlem1  30139  usgra2pth  30144  wwlkn0  30166  wlkiswwlk1  30167  wlkiswwlk2lem3  30170  wlklniswwlkn1  30176  wwlknextbi  30200  wwlknredwwlkn0  30202  wwlkextwrd  30203  wwlkextsur  30206  el2wlkonot  30231  el2spthonot  30232  el2spthonot0  30233  el2wlkonotot0  30234  el2wlkonotot1  30236  usg2spthonot0  30251  clwlkisclwwlklem2a4  30289  clwlkisclwwlklem2a  30290  clwwlkel  30298  clwwlkfo  30302  wwlkext2clwwlk  30308  clwwnisshclwwn  30316  eleclclwwlknlem2  30334  scshwfzeqfzo  30335  erclwwlkneqlen  30341  erclwwlkntr  30344  hashecclwwlkn1  30351  usghashecclwwlk  30352  clwlkfclwwlk  30360  clwlkfoclwwlk  30361  rusgraprop2  30397  wwlkextprop  30406  clwlknclwlkdifs  30421  1to2vfriswmgra  30441  frgrancvvdeqlem3  30468  frgrancvvdeqlem4  30469  frgrancvvdeqlemB  30474  frgrancvvdeqlemC  30475  usgreghash2spotv  30502  extwwlkfablem1  30510  extwwlkfablem2  30514  numclwwlkun  30515  numclwlk1lem2f1  30530  numclwwlk2lem1  30538  numclwlk2lem2f  30539  ztprmneprm  30580  psgnsn  30599  lmod0rng  30607  lincext3  30696  zlmodzxznm  30745  bj-snsetex  32036  bj-snglc  32042  opcon3b  32411  ps-1  32691  3atlem5  32701  4atex  33290
  Copyright terms: Public domain W3C validator