Theorem eqcoms 2748

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 2747	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 217	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  gencbvex  3553  sbceq2a  3816  eqimss2  4068  uneqdifeq  4516  tppreq3  4784  ifpprsnss  4789  tpprceq3  4829  preqsnd  4883  prproe  4929  copsex2t  5512  snopeqop  5525  opthhausdorff0  5537  relopabi  5846  cnvimassrndm  6183  cnveqb  6227  cnveq0  6228  unixpid  6315  reuop  6324  f0rn0  6806  fimadmfo  6843  f1ssf1  6894  tz6.12i  6948  fveqdmss  7112  fvcofneq  7127  funopsn  7182  f1ocnvfv  7314  f1ocnvfvb  7315  cbvfo  7325  riotaeqimp  7431  ov6g  7614  tfindsg  7898  findsg  7937  mptcnfimad  8027  suppimacnv  8215  ectocld  8842  ecoptocl  8865  undifixp  8992  phplem3OLD  9282  f1dmvrnfibi  9409  f1vrnfibi  9410  updjud  10003  card1  10037  pr2neOLD  10074  prdom2  10075  sornom  10346  indpi  10976  ltlen  11391  eqlei  11400  squeeze0  12198  nn0ind-raph  12743  fzoopth  13812  injresinjlem  13837  fvf1tp  13840  modmuladd  13964  modmuladdnn0  13966  hashf1rn  14401  hashrabsn1  14423  hash1snb  14468  hashgt12el  14471  hashgt12el2  14472  hashfzp1  14480  hash2prde  14519  hash2pwpr  14525  fi1uzind  14556  brfi1indALT  14559  lswlgt0cl  14617  wrd2ind  14771  pfxccatin12lem2  14779  pfxccatin12lem3  14780  cshweqrep  14869  cshwsexaOLD  14873  scshwfzeqfzo  14875  cshimadifsn  14878  cshimadifsn0  14879  2swrd2eqwrdeq  15002  wwlktovfo  15007  rennim  15288  absmod0  15352  modfsummods  15841  mod2eq1n2dvds  16395  m1expe  16422  m1expo  16423  m1exp1  16424  nn0o1gt2  16429  flodddiv4  16461  cncongr1  16714  ge2nprmge4  16748  m1dvdsndvds  16845  cshwrepswhash1  17150  initoeu2lem1  18081  istos  18488  mgmsscl  18683  mndinvmod  18802  smndex1n0mnd  18947  symgfvne  19422  symgfix2  19458  symgextf1  19463  symgfixelsi  19477  psgnsn  19562  odbezout  19600  cntzcmnss  19883  frgpnabllem1  19915  ringinvnzdiv  20324  rngcinv  20659  psgndiflemB  21641  uvcendim  21890  mamufacex  22421  smatvscl  22551  mavmulsolcl  22578  mdetunilem8  22646  pm2mpfo  22841  chpscmat  22869  chmaidscmat  22875  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  txcn  23655  qtopeu  23745  reeff1o  26509  relogbcxpb  26848  logbgcd1irr  26855  fsumdvdsmul  27256  zabsle1  27358  2lgslem1c  27455  2lgsoddprmlem3  27476  2sq2  27495  2sqreultlem  27509  2sqreunnltlem  27512  2sqreulem3  27515  pntrlog2bndlem5  27643  sltlend  27834  upgrpredgv  29174  usgredg2vlem2  29261  ushgredgedg  29264  ushgredgedgloop  29266  uhgrspan1  29338  nb3grprlem1  29415  uvtxnbgrb  29436  cusgrsize2inds  29489  1egrvtxdg0  29547  uspgrloopvtxel  29552  finsumvtxdg2size  29586  rusgrpropnb  29619  ifpsnprss  29659  upgrwlkvtxedg  29681  uspgr2wlkeq  29682  wlkp1lem5  29713  wlkp1  29717  usgr2pth  29800  uspgrn2crct  29841  iswwlksnon  29886  wlkiswwlks1  29900  wlkiswwlks2lem3  29904  wwlksnextbi  29927  wwlksnredwwlkn0  29929  wwlksnextwrd  29930  wwlksnextsurj  29933  wwlksnextprop  29945  wspn0  29957  umgr2adedgwlkonALT  29980  umgr2adedgspth  29981  umgr2wlkon  29983  elwwlks2ons3  29988  elwwlks2on  29992  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlkf1lem3  30038  clwwlkfo  30082  eleclclwwlknlem2  30093  erclwwlkntr  30103  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  0wlkonlem1  30150  upgr1wlkdlem1  30177  1pthon2v  30185  upgr3v3e3cycl  30212  uhgr3cyclexlem  30213  upgr4cycl4dv4e  30217  eupth2lem3lem3  30262  eupth2lem3lem4  30263  1to2vfriswmgr  30311  frgrncvvdeqlem6  30336  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  frgrwopreglem2  30345  2clwwlk2clwwlk  30382  extwwlkfab  30384  numclwwlk1lem2f1  30389  numclwwlkovh  30405  numclwwlk2lem1  30408  numclwlk2lem2f  30409  cdj1i  32465  brabgaf  32630  br8d  32632  sgn3da  34506  spthcycl  35097  goalrlem  35364  goalr  35365  fmlasucdisj  35367  satffunlem  35369  satffunlem1lem1  35370  satffunlem1lem2  35371  satffunlem2lem1  35372  satffunlem2lem2  35374  mthmb  35549  br8  35718  br4  35720  bj-snsetex  36929  bj-snglc  36935  copsex2d  37105  poimirlem20  37600  poimirlem26  37606  poimirlem27  37607  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  indexdom  37694  ismgmOLD  37810  rngodm1dm2  37892  rngomndo  37895  rngoueqz  37900  zerdivemp1x  37907  opcon3b  39152  ps-1  39434  3atlem5  39444  4atex  40033  selvvvval  42540  prjspvs  42565  iscard4  43495  pr2cv  43510  pm13.192  44379  iotavalsb  44402  fourierdlem32  46060  fourierdlem49  46076  fourierdlem64  46091  elprneb  46944  fveqvfvv  46955  funressnfv  46958  f1cof1b  46992  nvelim  47038  afvpcfv0  47061  afv0nbfvbi  47066  fnbrafvb  47069  tz6.12-afv  47088  afvco2  47091  ndmaovg  47099  afv2orxorb  47143  tz6.12-afv2  47155  tz6.12i-afv2  47158  f1oresf1o2  47206  elsetpreimafvbi  47265  imasetpreimafvbijlemfo  47279  iccpartiltu  47296  fargshiftfv  47313  fargshiftf  47314  lswn0  47318  prsprel  47361  reupr  47396  2exopprim  47399  fmtnorec2lem  47416  2pwp1prm  47463  lighneallem2  47480  lighneallem3  47481  proththd  47488  nn0o1gt2ALTV  47568  evenltle  47591  sbgoldbwt  47651  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  clnbgrval  47696  dfvopnbgr2  47725  gricushgr  47770  clnbgrgrim  47786  grimedg  47787  uspgrlimlem1  47812  grlimgrtri  47820  uspgropssxp  47867  lmod0rng  47952  lidldomn1  47954  zlidlring  47957  rngcinvALTV  47999  ztprmneprm  48072  lincext3  48185  zlmodzxznm  48226  suppdm  48239  elfzolborelfzop1  48248  nn0sumshdiglemB  48354  itcovalsucov  48402  lines  48465  rrx2vlinest  48475  line2xlem  48487  itschlc0yqe  48494  itsclquadeu  48511