Theorem eqcoms 2738

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

Step	Hyp	Ref	Expression
1		eqcom 2737	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 216	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  gencbvex  3534  sbceq2a  3788  eqimss2  4040  uneqdifeq  4491  tppreq3  4762  ifpprsnss  4767  tpprceq3  4806  preqsnd  4858  elpr2elpr  4868  prproe  4905  copsex2t  5491  copsex2gOLD  5493  snopeqop  5505  opthhausdorff0  5517  relopabi  5821  cnvimassrndm  6150  cnveqb  6194  cnveq0  6195  unixpid  6282  reuop  6291  f0rn0  6775  fimadmfo  6813  f1ssf1  6864  tz6.12i  6918  fveqdmss  7079  fvcofneq  7093  funopsn  7147  f1ocnvfv  7278  f1ocnvfvb  7279  cbvfo  7289  riotaeqimp  7394  ov6g  7573  tfindsg  7852  findsg  7892  suppimacnv  8161  suppssOLD  8182  ectocld  8780  ecoptocl  8803  undifixp  8930  phplem3OLD  9221  f1dmvrnfibi  9338  f1vrnfibi  9339  updjud  9931  card1  9965  pr2neOLD  10002  prdom2  10003  sornom  10274  indpi  10904  ltlen  11319  eqlei  11328  squeeze0  12121  nn0ind-raph  12666  injresinjlem  13756  modmuladd  13882  modmuladdnn0  13884  hashf1rn  14316  hashrabsn1  14338  hash1snb  14383  hashgt12el  14386  hashgt12el2  14387  hashfzp1  14395  hash2prde  14435  hash2pwpr  14441  fi1uzind  14462  brfi1indALT  14465  lswlgt0cl  14523  wrd2ind  14677  pfxccatin12lem2  14685  pfxccatin12lem3  14686  cshweqrep  14775  cshwsexaOLD  14779  scshwfzeqfzo  14781  cshimadifsn  14784  cshimadifsn0  14785  2swrd2eqwrdeq  14908  wwlktovfo  14913  rennim  15190  absmod0  15254  modfsummods  15743  mod2eq1n2dvds  16294  m1expe  16321  m1expo  16322  m1exp1  16323  nn0o1gt2  16328  flodddiv4  16360  cncongr1  16608  ge2nprmge4  16642  m1dvdsndvds  16735  cshwrepswhash1  17040  initoeu2lem1  17968  istos  18375  mgmsscl  18570  mndinvmod  18689  smndex1n0mnd  18829  symgfvne  19289  symgfix2  19325  symgextf1  19330  symgfixelsi  19344  psgnsn  19429  odbezout  19467  cntzcmnss  19750  frgpnabllem1  19782  ringinvnzdiv  20189  psgndiflemB  21372  uvcendim  21621  mamufacex  22111  smatvscl  22246  mavmulsolcl  22273  mdetunilem8  22341  pm2mpfo  22536  chpscmat  22564  chmaidscmat  22570  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  txcn  23350  qtopeu  23440  reeff1o  26195  relogbcxpb  26528  logbgcd1irr  26535  zabsle1  27035  2lgslem1c  27132  2lgsoddprmlem3  27153  2sq2  27172  2sqreultlem  27186  2sqreunnltlem  27189  2sqreulem3  27192  pntrlog2bndlem5  27320  upgrpredgv  28666  usgredg2vlem2  28750  ushgredgedg  28753  ushgredgedgloop  28755  uhgrspan1  28827  nb3grprlem1  28904  uvtxnbgrb  28925  cusgrsize2inds  28977  1egrvtxdg0  29035  uspgrloopvtxel  29040  finsumvtxdg2size  29074  rusgrpropnb  29107  ifpsnprss  29147  upgrwlkvtxedg  29169  uspgr2wlkeq  29170  wlkp1lem5  29201  wlkp1  29205  usgr2pth  29288  uspgrn2crct  29329  iswwlksnon  29374  wlkiswwlks1  29388  wlkiswwlks2lem3  29392  wwlksnextbi  29415  wwlksnredwwlkn0  29417  wwlksnextwrd  29418  wwlksnextsurj  29421  wwlksnextprop  29433  wspn0  29445  umgr2adedgwlkonALT  29468  umgr2adedgspth  29469  umgr2wlkon  29471  elwwlks2ons3  29476  elwwlks2on  29480  clwlkclwwlklem2a4  29517  clwlkclwwlklem2a  29518  clwlkclwwlkf1lem3  29526  clwwlkfo  29570  eleclclwwlknlem2  29581  erclwwlkntr  29591  hashecclwwlkn1  29597  umgrhashecclwwlk  29598  0wlkonlem1  29638  upgr1wlkdlem1  29665  1pthon2v  29673  upgr3v3e3cycl  29700  uhgr3cyclexlem  29701  upgr4cycl4dv4e  29705  eupth2lem3lem3  29750  eupth2lem3lem4  29751  1to2vfriswmgr  29799  frgrncvvdeqlem6  29824  frgrncvvdeqlem8  29826  frgrncvvdeqlem9  29827  frgrwopreglem2  29833  2clwwlk2clwwlk  29870  extwwlkfab  29872  numclwwlk1lem2f1  29877  numclwwlkovh  29893  numclwwlk2lem1  29896  numclwlk2lem2f  29897  cdj1i  31953  brabgaf  32104  br8d  32106  sgn3da  33838  spthcycl  34418  goalrlem  34685  goalr  34686  fmlasucdisj  34688  satffunlem  34690  satffunlem1lem1  34691  satffunlem1lem2  34692  satffunlem2lem1  34693  satffunlem2lem2  34695  mthmb  34870  br8  35030  br4  35032  bj-snsetex  36147  bj-snglc  36153  copsex2d  36323  poimirlem20  36811  poimirlem26  36817  poimirlem27  36818  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem  36842  indexdom  36905  ismgmOLD  37021  rngodm1dm2  37103  rngomndo  37106  rngoueqz  37111  zerdivemp1x  37118  opcon3b  38369  ps-1  38651  3atlem5  38661  4atex  39250  selvvvval  41459  prjspvs  41654  iscard4  42586  pr2cv  42601  pm13.192  43471  iotavalsb  43494  fourierdlem32  45153  fourierdlem49  45169  fourierdlem64  45184  elprneb  46037  fveqvfvv  46048  funressnfv  46051  f1cof1b  46083  nvelim  46129  afvpcfv0  46152  afv0nbfvbi  46157  fnbrafvb  46160  tz6.12-afv  46179  afvco2  46182  ndmaovg  46190  afv2orxorb  46234  tz6.12-afv2  46246  tz6.12i-afv2  46249  f1oresf1o2  46297  fzoopth  46333  elsetpreimafvbi  46357  imasetpreimafvbijlemfo  46371  iccpartiltu  46388  fargshiftfv  46405  fargshiftf  46406  lswn0  46410  prsprel  46453  reupr  46488  2exopprim  46491  fmtnorec2lem  46508  2pwp1prm  46555  lighneallem2  46572  lighneallem3  46573  proththd  46580  nn0o1gt2ALTV  46660  evenltle  46683  sbgoldbwt  46743  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  isomushgr  46792  isomuspgrlem1  46793  uspgropssxp  46820  lmod0rng  46908  lidldomn1  46911  zlidlring  46914  rngcinv  46967  rngcinvALTV  46979  ztprmneprm  47111  lincext3  47224  zlmodzxznm  47265  suppdm  47278  elfzolborelfzop1  47287  nn0sumshdiglemB  47393  itcovalsucov  47441  lines  47504  rrx2vlinest  47514  line2xlem  47526  itschlc0yqe  47533  itsclquadeu  47550