Theorem eqcoms 2743

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 2742	. 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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  gencbvex  3520  sbceq2a  3777  eqimss2  4018  uneqdifeq  4468  tppreq3  4735  ifpprsnss  4740  tpprceq3  4780  preqsnd  4835  prproe  4881  copsex2t  5467  snopeqop  5481  opthhausdorff0  5493  relopabi  5801  cnvimassrndm  6141  cnveqb  6185  cnveq0  6186  unixpid  6273  reuop  6282  f0rn0  6762  fimadmfo  6798  f1ssf1  6849  tz6.12i  6903  fveqdmss  7067  fvcofneq  7082  funopsn  7137  f1ocnvfv  7270  f1ocnvfvb  7271  cbvfo  7281  riotaeqimp  7386  ov6g  7569  tfindsg  7854  findsg  7891  mptcnfimad  7983  suppimacnv  8171  ectocld  8796  ecoptocl  8819  undifixp  8946  phplem3OLD  9228  f1dmvrnfibi  9351  f1vrnfibi  9352  updjud  9946  card1  9980  pr2neOLD  10017  prdom2  10018  sornom  10289  indpi  10919  ltlen  11334  eqlei  11343  squeeze0  12143  nn0ind-raph  12691  fzoopth  13776  injresinjlem  13801  fvf1tp  13804  modmuladd  13929  modmuladdnn0  13931  hashf1rn  14368  hashrabsn1  14390  hash1snb  14435  hashgt12el  14438  hashgt12el2  14439  hashfzp1  14447  hash2prde  14486  hash2pwpr  14492  fi1uzind  14523  brfi1indALT  14526  lswlgt0cl  14585  wrd2ind  14739  pfxccatin12lem2  14747  pfxccatin12lem3  14748  cshweqrep  14837  cshwsexaOLD  14841  scshwfzeqfzo  14843  cshimadifsn  14846  cshimadifsn0  14847  2swrd2eqwrdeq  14970  wwlktovfo  14975  rennim  15256  absmod0  15320  modfsummods  15807  mod2eq1n2dvds  16364  m1expe  16391  m1expo  16392  m1exp1  16393  nn0o1gt2  16398  flodddiv4  16432  cncongr1  16684  ge2nprmge4  16718  m1dvdsndvds  16816  cshwrepswhash1  17120  initoeu2lem1  18025  istos  18426  mgmsscl  18621  mndinvmod  18740  smndex1n0mnd  18888  symgfvne  19360  symgfix2  19395  symgextf1  19400  symgfixelsi  19414  psgnsn  19499  odbezout  19537  cntzcmnss  19820  frgpnabllem1  19852  ringinvnzdiv  20259  rngcinv  20595  psgndiflemB  21558  uvcendim  21805  mamufacex  22332  smatvscl  22460  mavmulsolcl  22487  mdetunilem8  22555  pm2mpfo  22750  chpscmat  22778  chmaidscmat  22784  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  txcn  23562  qtopeu  23652  reeff1o  26407  relogbcxpb  26747  logbgcd1irr  26754  fsumdvdsmul  27155  zabsle1  27257  2lgslem1c  27354  2lgsoddprmlem3  27375  2sq2  27394  2sqreultlem  27408  2sqreunnltlem  27411  2sqreulem3  27414  pntrlog2bndlem5  27542  sltlend  27733  upgrpredgv  29064  usgredg2vlem2  29151  ushgredgedg  29154  ushgredgedgloop  29156  uhgrspan1  29228  nb3grprlem1  29305  uvtxnbgrb  29326  cusgrsize2inds  29379  1egrvtxdg0  29437  uspgrloopvtxel  29442  finsumvtxdg2size  29476  rusgrpropnb  29509  ifpsnprss  29549  upgrwlkvtxedg  29571  uspgr2wlkeq  29572  wlkp1lem5  29603  wlkp1  29607  usgr2pth  29692  uspgrn2crct  29736  iswwlksnon  29781  wlkiswwlks1  29795  wlkiswwlks2lem3  29799  wwlksnextbi  29822  wwlksnredwwlkn0  29824  wwlksnextwrd  29825  wwlksnextsurj  29828  wwlksnextprop  29840  wspn0  29852  umgr2adedgwlkonALT  29875  umgr2adedgspth  29876  umgr2wlkon  29878  elwwlks2ons3  29883  elwwlks2on  29887  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlkf1lem3  29933  clwwlkfo  29977  eleclclwwlknlem2  29988  erclwwlkntr  29998  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  0wlkonlem1  30045  upgr1wlkdlem1  30072  1pthon2v  30080  upgr3v3e3cycl  30107  uhgr3cyclexlem  30108  upgr4cycl4dv4e  30112  eupth2lem3lem3  30157  eupth2lem3lem4  30158  1to2vfriswmgr  30206  frgrncvvdeqlem6  30231  frgrncvvdeqlem8  30233  frgrncvvdeqlem9  30234  frgrwopreglem2  30240  2clwwlk2clwwlk  30277  extwwlkfab  30279  numclwwlk1lem2f1  30284  numclwwlkovh  30300  numclwwlk2lem1  30303  numclwlk2lem2f  30304  cdj1i  32360  brabgaf  32534  br8d  32536  sgn3da  32759  spthcycl  35097  goalrlem  35364  goalr  35365  fmlasucdisj  35367  satffunlem  35369  satffunlem1lem1  35370  satffunlem1lem2  35371  satffunlem2lem1  35372  satffunlem2lem2  35374  mthmb  35549  br8  35719  br4  35721  bj-snsetex  36927  bj-snglc  36933  copsex2d  37103  poimirlem20  37610  poimirlem26  37616  poimirlem27  37617  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem  37641  indexdom  37704  ismgmOLD  37820  rngodm1dm2  37902  rngomndo  37905  rngoueqz  37910  zerdivemp1x  37917  opcon3b  39160  ps-1  39442  3atlem5  39452  4atex  40041  selvvvval  42555  prjspvs  42580  iscard4  43504  pr2cv  43519  pm13.192  44382  iotavalsb  44405  relpfrlem  44926  fourierdlem32  46116  fourierdlem49  46132  fourierdlem64  46147  elprneb  47006  fveqvfvv  47017  funressnfv  47020  f1cof1b  47054  nvelim  47100  afvpcfv0  47123  afv0nbfvbi  47128  fnbrafvb  47131  tz6.12-afv  47150  afvco2  47153  ndmaovg  47161  afv2orxorb  47205  tz6.12-afv2  47217  tz6.12i-afv2  47220  f1oresf1o2  47268  elsetpreimafvbi  47353  imasetpreimafvbijlemfo  47367  iccpartiltu  47384  fargshiftfv  47401  fargshiftf  47402  lswn0  47406  prsprel  47449  reupr  47484  2exopprim  47487  fmtnorec2lem  47504  2pwp1prm  47551  lighneallem2  47568  lighneallem3  47569  proththd  47576  nn0o1gt2ALTV  47656  evenltle  47679  sbgoldbwt  47739  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  clnbgrval  47784  dfvopnbgr2  47814  uhgrimedgi  47851  gricushgr  47878  clnbgrgrim  47895  grimedg  47896  cycl3grtri  47907  isubgr3stgrlem4  47929  uspgrlimlem1  47948  grlimgrtri  47956  uspgropssxp  48067  lmod0rng  48152  lidldomn1  48154  zlidlring  48157  rngcinvALTV  48199  ztprmneprm  48270  lincext3  48380  zlmodzxznm  48421  suppdm  48434  elfzolborelfzop1  48443  nn0sumshdiglemB  48548  itcovalsucov  48596  lines  48659  rrx2vlinest  48669  line2xlem  48681  itschlc0yqe  48688  itsclquadeu  48705