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  39280  iscard4  39920  pr2cv  39927  pm13.192  40762  iotavalsb  40785  fourierdlem32  42444  fourierdlem49  42460  fourierdlem64  42475  elprneb  43284  fveqvfvv  43295  funressnfv  43298  nvelim  43342  afvpcfv0  43365  afv0nbfvbi  43370  fnbrafvb  43373  tz6.12-afv  43392  afvco2  43395  ndmaovg  43403  afv2orxorb  43447  tz6.12-afv2  43459  tz6.12i-afv2  43462  f1oresf1o2  43510  fzoopth  43547  elsetpreimafvbi  43571  imasetpreimafvbijlemfo  43585  iccpartiltu  43602  fargshiftfv  43619  fargshiftf  43620  lswn0  43624  prsprel  43669  reupr  43704  2exopprim  43707  fmtnorec2lem  43724  2pwp1prm  43771  lighneallem2  43791  lighneallem3  43792  proththd  43799  nn0o1gt2ALTV  43879  evenltle  43902  sbgoldbwt  43962  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  isomushgr  44011  isomuspgrlem1  44012  uspgropssxp  44039  lmod0rng  44159  lidldomn1  44212  zlidlring  44219  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347  ztprmneprm  44415  lincext3  44531  zlmodzxznm  44572  suppdm  44585  elfzolborelfzop1  44594  nn0sumshdiglemB  44700  lines  44738  rrx2vlinest  44748  line2xlem  44760  itschlc0yqe  44767  itsclquadeu  44784