Theorem eqcoms 2829

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 2828	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 219	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 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  gencbvex  3549  sbceq2a  3784  eqimss2  4024  uneqdifeq  4438  tppreq3  4695  ifpprsnss  4700  tpprceq3  4737  preqsnd  4789  elpr2elpr  4799  prproe  4836  copsex2t  5383  copsex2g  5384  snopeqop  5396  opthhausdorff0  5408  relopabi  5694  cnveqb  6053  cnveq0  6054  unixpid  6135  reuop  6144  f0rn0  6564  fimadmfo  6599  f1ssf1  6646  tz6.12i  6696  fveqdmss  6846  fvcofneq  6859  funopsn  6910  f1ocnvfv  7035  f1ocnvfvb  7036  cbvfo  7045  riotaeqimp  7140  ov6g  7312  tfindsg  7575  findsg  7609  suppimacnv  7841  suppss  7860  ectocld  8364  ecoptocl  8387  undifixp  8498  phplem3  8698  f1dmvrnfibi  8808  f1vrnfibi  8809  updjud  9363  card1  9397  pr2ne  9431  prdom2  9432  sornom  9699  indpi  10329  ltlen  10741  eqlei  10750  squeeze0  11543  nn0ind-raph  12083  injresinjlem  13158  modmuladd  13282  modmuladdnn0  13284  hashf1rn  13714  hashrabsn1  13736  hash1snb  13781  hashgt12el  13784  hashgt12el2  13785  hashfzp1  13793  hash2prde  13829  hash2pwpr  13835  fi1uzind  13856  brfi1indALT  13859  lswlgt0cl  13921  wrd2ind  14085  pfxccatin12lem2  14093  pfxccatin12lem3  14094  cshweqrep  14183  cshwsexa  14186  scshwfzeqfzo  14188  cshimadifsn  14191  cshimadifsn0  14192  2swrd2eqwrdeq  14315  wwlktovfo  14322  rennim  14598  absmod0  14663  modfsummods  15148  mod2eq1n2dvds  15696  m1expe  15725  m1expo  15726  m1exp1  15727  nn0o1gt2  15732  flodddiv4  15764  cncongr1  16011  ge2nprmge4  16045  m1dvdsndvds  16135  cshwrepswhash1  16436  initoeu2lem1  17274  istos  17645  mgmsscl  17857  mndinvmod  17941  smndex1n0mnd  18077  symgfvne  18509  symgfix2  18544  symgextf1  18549  symgfixelsi  18563  psgnsn  18648  odbezout  18685  cntzcmnss  18961  frgpnabllem1  18993  ringinvnzdiv  19343  psgndiflemB  20744  uvcendim  20991  mamufacex  21000  smatvscl  21133  mavmulsolcl  21160  mdetunilem8  21228  pm2mpfo  21422  chpscmat  21450  chmaidscmat  21456  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  txcn  22234  qtopeu  22324  reeff1o  25035  relogbcxpb  25365  logbgcd1irr  25372  zabsle1  25872  2lgslem1c  25969  2lgsoddprmlem3  25990  2sq2  26009  2sqreultlem  26023  2sqreunnltlem  26026  2sqreulem3  26029  pntrlog2bndlem5  26157  upgrpredgv  26924  usgredg2vlem2  27008  ushgredgedg  27011  ushgredgedgloop  27013  uhgrspan1  27085  nb3grprlem1  27162  uvtxnbgrb  27183  cusgrsize2inds  27235  1egrvtxdg0  27293  uspgrloopvtxel  27298  finsumvtxdg2size  27332  rusgrpropnb  27365  ifpsnprss  27404  upgrwlkvtxedg  27426  uspgr2wlkeq  27427  wlkp1lem5  27459  wlkp1  27463  usgr2pth  27545  uspgrn2crct  27586  iswwlksnon  27631  wlkiswwlks1  27645  wlkiswwlks2lem3  27649  wwlksnextbi  27672  wwlksnredwwlkn0  27674  wwlksnextwrd  27675  wwlksnextsurj  27678  wwlksnextprop  27691  wspn0  27703  umgr2adedgwlkonALT  27726  umgr2adedgspth  27727  umgr2wlkon  27729  elwwlks2ons3  27734  elwwlks2on  27738  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlkf1lem3  27784  clwwlkfo  27829  eleclclwwlknlem2  27840  erclwwlkntr  27850  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  0wlkonlem1  27897  upgr1wlkdlem1  27924  1pthon2v  27932  upgr3v3e3cycl  27959  uhgr3cyclexlem  27960  upgr4cycl4dv4e  27964  eupth2lem3lem3  28009  eupth2lem3lem4  28010  1to2vfriswmgr  28058  frgrncvvdeqlem6  28083  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  frgrwopreglem2  28092  2clwwlk2clwwlk  28129  extwwlkfab  28131  numclwwlk1lem2f1  28136  numclwwlkovh  28152  numclwwlk2lem1  28155  numclwlk2lem2f  28156  cdj1i  30210  brabgaf  30359  br8d  30361  sgn3da  31799  spthcycl  32376  goalrlem  32643  goalr  32644  fmlasucdisj  32646  satffunlem  32648  satffunlem1lem1  32649  satffunlem1lem2  32650  satffunlem2lem1  32651  satffunlem2lem2  32653  mthmb  32828  br8  32992  br4  32994  bj-snsetex  34278  bj-snglc  34284  copsex2d  34434  poimirlem20  34927  poimirlem26  34933  poimirlem27  34934  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem  34958  indexdom  35024  ismgmOLD  35143  rngodm1dm2  35225  rngomndo  35228  rngoueqz  35233  zerdivemp1x  35240  opcon3b  36347  ps-1  36628  3atlem5  36638  4atex  37227  prjspvs  39309  iscard4  39949  pr2cv  39956  pm13.192  40791  iotavalsb  40814  fourierdlem32  42473  fourierdlem49  42489  fourierdlem64  42504  elprneb  43313  fveqvfvv  43324  funressnfv  43327  nvelim  43371  afvpcfv0  43394  afv0nbfvbi  43399  fnbrafvb  43402  tz6.12-afv  43421  afvco2  43424  ndmaovg  43432  afv2orxorb  43476  tz6.12-afv2  43488  tz6.12i-afv2  43491  f1oresf1o2  43539  fzoopth  43576  elsetpreimafvbi  43600  imasetpreimafvbijlemfo  43614  iccpartiltu  43631  fargshiftfv  43648  fargshiftf  43649  lswn0  43653  prsprel  43698  reupr  43733  2exopprim  43736  fmtnorec2lem  43753  2pwp1prm  43800  lighneallem2  43820  lighneallem3  43821  proththd  43828  nn0o1gt2ALTV  43908  evenltle  43931  sbgoldbwt  43991  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  isomushgr  44040  isomuspgrlem1  44041  uspgropssxp  44068  lmod0rng  44188  lidldomn1  44241  zlidlring  44248  rngcinv  44301  rngcinvALTV  44313  ringcinv  44352  ringcinvALTV  44376  ztprmneprm  44444  lincext3  44560  zlmodzxznm  44601  suppdm  44614  elfzolborelfzop1  44623  nn0sumshdiglemB  44729  lines  44767  rrx2vlinest  44777  line2xlem  44789  itschlc0yqe  44796  itsclquadeu  44813