Theorem eqcoms 2786

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

Syntax hints:   → wi 4   = wceq 1601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770

This theorem is referenced by:  gencbvex  3452  sbceq2a  3664  eqimss2  3877  uneqdifeq  4281  tppreq3  4526  ifpprsnss  4531  tpprceq3  4568  preqsnd  4622  elpr2elpr  4634  prproe  4671  copsex2t  5190  copsex2g  5191  snopeqop  5204  opthhausdorff0  5217  relopabi  5493  cnveqb  5845  cnveq0  5846  unixpid  5926  f0rn0  6342  fimadmfo  6377  f1ssf1  6424  tz6.12i  6474  fveqdmss  6620  fvcofneq  6633  funopsn  6681  f1ocnvfv  6808  f1ocnvfvb  6809  cbvfo  6818  riotaeqimp  6908  ov6g  7077  tfindsg  7340  findsg  7373  suppimacnv  7589  suppss  7609  ectocld  8099  ecoptocl  8122  undifixp  8232  phplem3  8431  f1dmvrnfibi  8540  f1vrnfibi  8541  updjud  9095  card1  9129  pr2ne  9163  prdom2  9164  sornom  9436  indpi  10066  ltlen  10479  eqlei  10488  squeeze0  11282  nn0ind-raph  11833  injresinjlem  12911  modmuladd  13035  modmuladdnn0  13037  hashf1rn  13462  hashrabsn1  13482  hash1snb  13525  hashgt12el  13528  hashgt12el2  13529  hashfzp1  13536  hash2prde  13570  hash2pwpr  13576  fi1uzind  13597  brfi1indALT  13600  lswlgt0cl  13663  pfxsuffeqwrdeq  13811  wrd2ind  13848  wrd2indOLD  13849  reuccats1lemOLD  13851  pfxccatin12lem2  13862  swrdccatin12lem2OLD  13863  swrdccatin12lem3  13864  swrdccat3aOLD  13874  cshweqrep  13976  cshwsexa  13979  scshwfzeqfzo  13981  cshimadifsn  13984  cshimadifsn0  13985  2swrd2eqwrdeq  14108  2swrd2eqwrdeqOLD  14109  wwlktovfo  14114  rennim  14390  absmod0  14454  modfsummods  14933  mod2eq1n2dvds  15479  m1expe  15508  m1expo  15509  m1exp1  15510  nn0o1gt2  15515  flodddiv4  15547  cncongr1  15790  m1dvdsndvds  15911  cshwrepswhash1  16212  xpsfrnel2  16615  initoeu2lem1  17053  istos  17425  symgfvne  18195  symgfix2  18223  symgextf1  18228  symgfixelsi  18242  psgnsn  18328  odbezout  18363  cntzcmnss  18636  frgpnabllem1  18666  ringinvnzdiv  18984  psgndiflemB  20346  uvcendim  20594  mamufacex  20603  smatvscl  20739  mavmulsolcl  20766  mdetunilem8  20834  pm2mpfo  21030  chpscmat  21058  chmaidscmat  21064  chfacfscmulgsum  21076  chfacfpmmulgsum  21080  txcn  21842  qtopeu  21932  reeff1o  24642  relogbcxpb  24969  logbgcd1irr  24976  zabsle1  25477  2lgslem1c  25574  2lgsoddprmlem3  25595  pntrlog2bndlem5  25726  upgrpredgv  26492  usgredg2vlem2  26576  ushgredgedg  26579  ushgredgedgloop  26581  ushgredgedgloopOLD  26582  uhgrspan1  26654  nb3grprlem1  26732  uvtxnbgrb  26753  cusgrsize2inds  26805  1egrvtxdg0  26863  uspgrloopvtxel  26868  finsumvtxdg2size  26902  rusgrpropnb  26935  ifpsnprss  26974  upgrwlkvtxedg  26996  uspgr2wlkeq  26997  wlkp1lem5  27032  wlkp1  27036  usgr2pth  27120  uspgrn2crct  27161  iswwlksnon  27206  wlkiswwlks1  27220  wlkiswwlks2lem3  27224  wwlksnextbi  27259  wwlksnextbiOLD  27260  wwlksnredwwlkn0  27263  wwlksnredwwlkn0OLD  27264  wwlksnextwrd  27265  wwlksnextsurj  27268  wwlksnextwrdOLD  27270  wwlksnextsurOLD  27273  wwlksnextprop  27293  wwlksnextpropOLD  27294  wspn0  27308  umgr2adedgwlkonALT  27331  umgr2adedgspth  27332  umgr2wlkon  27334  elwwlks2ons3  27339  elwwlks2on  27343  clwlkclwwlklem2a4  27381  clwlkclwwlklem2a  27382  clwlkclwwlkf1lem3  27393  clwlkclwwlkf1lem3OLD  27394  clwwlkel  27441  clwwlkfoOLD  27445  clwwlkfo  27450  wwlksext2clwwlk  27458  eleclclwwlknlem2  27463  erclwwlkntr  27473  hashecclwwlkn1  27479  umgrhashecclwwlk  27480  clwwlknonwwlknonb  27512  0wlkonlem1  27525  upgr1wlkdlem1  27552  1pthon2v  27560  upgr3v3e3cycl  27587  uhgr3cyclexlem  27588  upgr4cycl4dv4e  27592  eupth2lem3lem3  27638  eupth2lem3lem4  27639  1to2vfriswmgr  27691  frgrncvvdeqlem6  27716  frgrncvvdeqlem8  27718  frgrncvvdeqlem9  27719  frgrwopreglem2  27725  2clwwlk2clwwlk  27765  2clwwlk2clwwlkOLD  27766  extwwlkfab  27769  extwwlkfabOLD  27770  numclwwlk1lem2f1  27777  numclwwlk1lem2f1OLD  27782  numclwwlkovh  27805  numclwwlk2lem1  27808  numclwlk2lem2f  27809  numclwlk2lem2fOLD  27812  cdj1i  29868  brabgaf  29987  br8d  29989  sgn3da  31206  mthmb  32081  br8  32244  br4  32246  bj-snsetex  33527  bj-snglc  33533  poimirlem20  34060  poimirlem26  34066  poimirlem27  34067  mblfinlem3  34079  mblfinlem4  34080  itg2addnclem  34091  indexdom  34159  ismgmOLD  34278  rngodm1dm2  34360  rngomndo  34363  rngoueqz  34368  zerdivemp1x  34375  opcon3b  35355  ps-1  35636  3atlem5  35646  4atex  36235  pm13.192  39576  iotavalsb  39599  fourierdlem32  41293  fourierdlem49  41309  fourierdlem64  41324  elprneb  42108  fveqvfvv  42114  funressnfv  42117  nvelim  42174  afvpcfv0  42197  afv0nbfvbi  42202  fnbrafvb  42205  tz6.12-afv  42224  afvco2  42227  ndmaovg  42235  afv2orxorb  42279  tz6.12-afv2  42291  tz6.12i-afv2  42294  f1oresf1o2  42342  fzoopth  42379  iccpartiltu  42400  fargshiftfv  42417  fargshiftf  42418  lswn0  42422  prsprel  42436  fmtnorec2lem  42485  2pwp1prm  42534  lighneallem2  42554  lighneallem3  42555  proththd  42562  nn0o1gt2ALTV  42640  evenltle  42661  sbgoldbwt  42700  nnsum4primeseven  42723  nnsum4primesevenALTV  42724  isomushgr  42749  isomuspgrlem1  42750  uspgropssxp  42777  lmod0rng  42893  lidldomn1  42946  zlidlring  42953  rngcinv  43006  rngcinvALTV  43018  ringcinv  43057  ringcinvALTV  43081  ztprmneprm  43150  lincext3  43270  zlmodzxznm  43311  suppdm  43325  elfzolborelfzop1  43334  nn0sumshdiglemB  43439  lines  43477  rrx2vlinest  43487  line2xlem  43499  itschlc0yqe  43506  itsclquadeu  43523