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

Theorem eqcoms 2827
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 2826 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 219 1 (𝐵 = 𝐴𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812
This theorem is referenced by:  gencbvex  3548  sbceq2a  3782  eqimss2  4022  uneqdifeq  4436  tppreq3  4687  ifpprsnss  4692  tpprceq3  4729  preqsnd  4781  elpr2elpr  4791  prproe  4828  copsex2t  5374  copsex2g  5375  snopeqop  5387  opthhausdorff0  5399  relopabi  5687  cnveqb  6046  cnveq0  6047  unixpid  6128  reuop  6137  f0rn0  6557  fimadmfo  6592  f1ssf1  6639  tz6.12i  6689  fveqdmss  6839  fvcofneq  6852  funopsn  6903  f1ocnvfv  7027  f1ocnvfvb  7028  cbvfo  7037  riotaeqimp  7132  ov6g  7304  tfindsg  7567  findsg  7601  suppimacnv  7833  suppss  7852  ectocld  8356  ecoptocl  8379  undifixp  8490  phplem3  8690  f1dmvrnfibi  8800  f1vrnfibi  8801  updjud  9355  card1  9389  pr2ne  9423  prdom2  9424  sornom  9691  indpi  10321  ltlen  10733  eqlei  10742  squeeze0  11535  nn0ind-raph  12074  injresinjlem  13149  modmuladd  13273  modmuladdnn0  13275  hashf1rn  13705  hashrabsn1  13727  hash1snb  13772  hashgt12el  13775  hashgt12el2  13776  hashfzp1  13784  hash2prde  13820  hash2pwpr  13826  fi1uzind  13847  brfi1indALT  13850  lswlgt0cl  13913  wrd2ind  14077  pfxccatin12lem2  14085  pfxccatin12lem3  14086  cshweqrep  14175  cshwsexa  14178  scshwfzeqfzo  14180  cshimadifsn  14183  cshimadifsn0  14184  2swrd2eqwrdeq  14307  wwlktovfo  14314  rennim  14590  absmod0  14655  modfsummods  15140  mod2eq1n2dvds  15688  m1expe  15717  m1expo  15718  m1exp1  15719  nn0o1gt2  15724  flodddiv4  15756  cncongr1  16003  ge2nprmge4  16037  m1dvdsndvds  16127  cshwrepswhash1  16428  initoeu2lem1  17266  istos  17637  mgmsscl  17849  mndinvmod  17933  smndex1n0mnd  18069  symgfvne  18501  symgfix2  18536  symgextf1  18541  symgfixelsi  18555  psgnsn  18640  odbezout  18677  cntzcmnss  18953  frgpnabllem1  18985  ringinvnzdiv  19335  psgndiflemB  20736  uvcendim  20983  mamufacex  20992  smatvscl  21125  mavmulsolcl  21152  mdetunilem8  21220  pm2mpfo  21414  chpscmat  21442  chmaidscmat  21448  chfacfscmulgsum  21460  chfacfpmmulgsum  21464  txcn  22226  qtopeu  22316  reeff1o  25027  relogbcxpb  25357  logbgcd1irr  25364  zabsle1  25864  2lgslem1c  25961  2lgsoddprmlem3  25982  2sq2  26001  2sqreultlem  26015  2sqreunnltlem  26018  2sqreulem3  26021  pntrlog2bndlem5  26149  upgrpredgv  26916  usgredg2vlem2  27000  ushgredgedg  27003  ushgredgedgloop  27005  uhgrspan1  27077  nb3grprlem1  27154  uvtxnbgrb  27175  cusgrsize2inds  27227  1egrvtxdg0  27285  uspgrloopvtxel  27290  finsumvtxdg2size  27324  rusgrpropnb  27357  ifpsnprss  27396  upgrwlkvtxedg  27418  uspgr2wlkeq  27419  wlkp1lem5  27451  wlkp1  27455  usgr2pth  27537  uspgrn2crct  27578  iswwlksnon  27623  wlkiswwlks1  27637  wlkiswwlks2lem3  27641  wwlksnextbi  27664  wwlksnredwwlkn0  27666  wwlksnextwrd  27667  wwlksnextsurj  27670  wwlksnextprop  27683  wspn0  27695  umgr2adedgwlkonALT  27718  umgr2adedgspth  27719  umgr2wlkon  27721  elwwlks2ons3  27726  elwwlks2on  27730  clwlkclwwlklem2a4  27767  clwlkclwwlklem2a  27768  clwlkclwwlkf1lem3  27776  clwwlkfo  27821  eleclclwwlknlem2  27832  erclwwlkntr  27842  hashecclwwlkn1  27848  umgrhashecclwwlk  27849  0wlkonlem1  27889  upgr1wlkdlem1  27916  1pthon2v  27924  upgr3v3e3cycl  27951  uhgr3cyclexlem  27952  upgr4cycl4dv4e  27956  eupth2lem3lem3  28001  eupth2lem3lem4  28002  1to2vfriswmgr  28050  frgrncvvdeqlem6  28075  frgrncvvdeqlem8  28077  frgrncvvdeqlem9  28078  frgrwopreglem2  28084  2clwwlk2clwwlk  28121  extwwlkfab  28123  numclwwlk1lem2f1  28128  numclwwlkovh  28144  numclwwlk2lem1  28147  numclwlk2lem2f  28148  cdj1i  30202  brabgaf  30351  br8d  30353  sgn3da  31792  spthcycl  32369  goalrlem  32636  goalr  32637  fmlasucdisj  32639  satffunlem  32641  satffunlem1lem1  32642  satffunlem1lem2  32643  satffunlem2lem1  32644  satffunlem2lem2  32646  mthmb  32821  br8  32985  br4  32987  bj-snsetex  34268  bj-snglc  34274  copsex2d  34423  poimirlem20  34904  poimirlem26  34910  poimirlem27  34911  mblfinlem3  34923  mblfinlem4  34924  itg2addnclem  34935  indexdom  35001  ismgmOLD  35120  rngodm1dm2  35202  rngomndo  35205  rngoueqz  35210  zerdivemp1x  35217  opcon3b  36324  ps-1  36605  3atlem5  36615  4atex  37204  prjspvs  39250  iscard4  39890  pr2cv  39897  pm13.192  40732  iotavalsb  40755  fourierdlem32  42414  fourierdlem49  42430  fourierdlem64  42445  elprneb  43254  fveqvfvv  43265  funressnfv  43268  nvelim  43312  afvpcfv0  43335  afv0nbfvbi  43340  fnbrafvb  43343  tz6.12-afv  43362  afvco2  43365  ndmaovg  43373  afv2orxorb  43417  tz6.12-afv2  43429  tz6.12i-afv2  43432  f1oresf1o2  43480  fzoopth  43517  elsetpreimafvbi  43541  imasetpreimafvbijlemfo  43555  iccpartiltu  43572  fargshiftfv  43589  fargshiftf  43590  lswn0  43594  prsprel  43639  reupr  43674  2exopprim  43677  fmtnorec2lem  43694  2pwp1prm  43741  lighneallem2  43761  lighneallem3  43762  proththd  43769  nn0o1gt2ALTV  43849  evenltle  43872  sbgoldbwt  43932  nnsum4primeseven  43955  nnsum4primesevenALTV  43956  isomushgr  43981  isomuspgrlem1  43982  uspgropssxp  44009  lmod0rng  44129  lidldomn1  44182  zlidlring  44189  rngcinv  44242  rngcinvALTV  44254  ringcinv  44293  ringcinvALTV  44317  ztprmneprm  44385  lincext3  44501  zlmodzxznm  44542  suppdm  44555  elfzolborelfzop1  44564  nn0sumshdiglemB  44670  lines  44708  rrx2vlinest  44718  line2xlem  44730  itschlc0yqe  44737  itsclquadeu  44754
  Copyright terms: Public domain W3C validator