Theorem eqcoms 2737

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

Syntax hints:   → wi 4   = wceq 1540

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  gencbvex  3507  sbceq2a  3765  eqimss2  4006  uneqdifeq  4456  tppreq3  4723  ifpprsnss  4728  tpprceq3  4768  preqsnd  4823  prproe  4869  copsex2t  5452  snopeqop  5466  opthhausdorff0  5478  relopabi  5785  cnvimassrndm  6125  cnveqb  6169  cnveq0  6170  unixpid  6257  reuop  6266  f0rn0  6745  fimadmfo  6781  f1ssf1  6832  tz6.12i  6886  fveqdmss  7050  fvcofneq  7065  funopsn  7120  f1ocnvfv  7253  f1ocnvfvb  7254  cbvfo  7264  riotaeqimp  7370  ov6g  7553  tfindsg  7837  findsg  7873  mptcnfimad  7965  suppimacnv  8153  ectocld  8755  ecoptocl  8780  undifixp  8907  f1dmvrnfibi  9292  f1vrnfibi  9293  updjud  9887  card1  9921  pr2neOLD  9958  prdom2  9959  sornom  10230  indpi  10860  ltlen  11275  eqlei  11284  squeeze0  12086  nn0ind-raph  12634  fzoopth  13723  injresinjlem  13748  fvf1tp  13751  modmuladd  13878  modmuladdnn0  13880  hashf1rn  14317  hashrabsn1  14339  hash1snb  14384  hashgt12el  14387  hashgt12el2  14388  hashfzp1  14396  hash2prde  14435  hash2pwpr  14441  fi1uzind  14472  brfi1indALT  14475  lswlgt0cl  14534  wrd2ind  14688  pfxccatin12lem2  14696  pfxccatin12lem3  14697  cshweqrep  14786  cshwsexaOLD  14790  scshwfzeqfzo  14792  cshimadifsn  14795  cshimadifsn0  14796  2swrd2eqwrdeq  14919  wwlktovfo  14924  rennim  15205  absmod0  15269  modfsummods  15759  mod2eq1n2dvds  16317  m1expe  16344  m1expo  16345  m1exp1  16346  nn0o1gt2  16351  flodddiv4  16385  cncongr1  16637  ge2nprmge4  16671  m1dvdsndvds  16769  cshwrepswhash1  17073  initoeu2lem1  17976  istos  18377  mgmsscl  18572  mndinvmod  18691  smndex1n0mnd  18839  symgfvne  19311  symgfix2  19346  symgextf1  19351  symgfixelsi  19365  psgnsn  19450  odbezout  19488  cntzcmnss  19771  frgpnabllem1  19803  ringinvnzdiv  20210  rngcinv  20546  psgndiflemB  21509  uvcendim  21756  mamufacex  22283  smatvscl  22411  mavmulsolcl  22438  mdetunilem8  22506  pm2mpfo  22701  chpscmat  22729  chmaidscmat  22735  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  txcn  23513  qtopeu  23603  reeff1o  26357  relogbcxpb  26697  logbgcd1irr  26704  fsumdvdsmul  27105  zabsle1  27207  2lgslem1c  27304  2lgsoddprmlem3  27325  2sq2  27344  2sqreultlem  27358  2sqreunnltlem  27361  2sqreulem3  27364  pntrlog2bndlem5  27492  sltlend  27683  upgrpredgv  29066  usgredg2vlem2  29153  ushgredgedg  29156  ushgredgedgloop  29158  uhgrspan1  29230  nb3grprlem1  29307  uvtxnbgrb  29328  cusgrsize2inds  29381  1egrvtxdg0  29439  uspgrloopvtxel  29444  finsumvtxdg2size  29478  rusgrpropnb  29511  ifpsnprss  29551  upgrwlkvtxedg  29573  uspgr2wlkeq  29574  wlkp1lem5  29605  wlkp1  29609  usgr2pth  29694  uspgrn2crct  29738  iswwlksnon  29783  wlkiswwlks1  29797  wlkiswwlks2lem3  29801  wwlksnextbi  29824  wwlksnredwwlkn0  29826  wwlksnextwrd  29827  wwlksnextsurj  29830  wwlksnextprop  29842  wspn0  29854  umgr2adedgwlkonALT  29877  umgr2adedgspth  29878  umgr2wlkon  29880  elwwlks2ons3  29885  elwwlks2on  29889  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlkf1lem3  29935  clwwlkfo  29979  eleclclwwlknlem2  29990  erclwwlkntr  30000  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  0wlkonlem1  30047  upgr1wlkdlem1  30074  1pthon2v  30082  upgr3v3e3cycl  30109  uhgr3cyclexlem  30110  upgr4cycl4dv4e  30114  eupth2lem3lem3  30159  eupth2lem3lem4  30160  1to2vfriswmgr  30208  frgrncvvdeqlem6  30233  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  frgrwopreglem2  30242  2clwwlk2clwwlk  30279  extwwlkfab  30281  numclwwlk1lem2f1  30286  numclwwlkovh  30302  numclwwlk2lem1  30305  numclwlk2lem2f  30306  cdj1i  32362  brabgaf  32536  br8d  32538  sgn3da  32759  onvf1odlem1  35090  spthcycl  35116  goalrlem  35383  goalr  35384  fmlasucdisj  35386  satffunlem  35388  satffunlem1lem1  35389  satffunlem1lem2  35390  satffunlem2lem1  35391  satffunlem2lem2  35393  mthmb  35568  br8  35743  br4  35745  bj-snsetex  36951  bj-snglc  36957  copsex2d  37127  poimirlem20  37634  poimirlem26  37640  poimirlem27  37641  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  indexdom  37728  ismgmOLD  37844  rngodm1dm2  37926  rngomndo  37929  rngoueqz  37934  zerdivemp1x  37941  opcon3b  39189  ps-1  39471  3atlem5  39481  4atex  40070  selvvvval  42573  prjspvs  42598  iscard4  43522  pr2cv  43537  pm13.192  44399  iotavalsb  44422  relpfrlem  44943  fourierdlem32  46137  fourierdlem49  46153  fourierdlem64  46168  elprneb  47030  fveqvfvv  47041  funressnfv  47044  f1cof1b  47078  nvelim  47124  afvpcfv0  47147  afv0nbfvbi  47152  fnbrafvb  47155  tz6.12-afv  47174  afvco2  47177  ndmaovg  47185  afv2orxorb  47229  tz6.12-afv2  47241  tz6.12i-afv2  47244  f1oresf1o2  47292  elsetpreimafvbi  47392  imasetpreimafvbijlemfo  47406  iccpartiltu  47423  fargshiftfv  47440  fargshiftf  47441  lswn0  47445  prsprel  47488  reupr  47523  2exopprim  47526  fmtnorec2lem  47543  2pwp1prm  47590  lighneallem2  47607  lighneallem3  47608  proththd  47615  nn0o1gt2ALTV  47695  evenltle  47718  sbgoldbwt  47778  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  clnbgrval  47823  dfvopnbgr2  47853  uhgrimedgi  47890  gricushgr  47917  clnbgrgrim  47934  grimedg  47935  cycl3grtri  47946  isubgr3stgrlem4  47968  uspgrlimlem1  47987  grlimgrtri  47995  gpgedg2ov  48057  gpgedg2iv  48058  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  uspgropssxp  48132  lmod0rng  48217  lidldomn1  48219  zlidlring  48222  rngcinvALTV  48264  ztprmneprm  48335  lincext3  48445  zlmodzxznm  48486  suppdm  48499  elfzolborelfzop1  48508  nn0sumshdiglemB  48609  itcovalsucov  48657  lines  48720  rrx2vlinest  48730  line2xlem  48742  itschlc0yqe  48749  itsclquadeu  48766