Theorem eqcoms 2741

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  gencbvex  3536  sbceq2a  3789  eqimss2  4041  uneqdifeq  4492  tppreq3  4763  ifpprsnss  4768  tpprceq3  4807  preqsnd  4859  elpr2elpr  4869  prproe  4906  copsex2t  5492  copsex2gOLD  5494  snopeqop  5506  opthhausdorff0  5518  relopabi  5821  cnvimassrndm  6149  cnveqb  6193  cnveq0  6194  unixpid  6281  reuop  6290  f0rn0  6774  fimadmfo  6812  f1ssf1  6863  tz6.12i  6917  fveqdmss  7078  fvcofneq  7092  funopsn  7143  f1ocnvfv  7273  f1ocnvfvb  7274  cbvfo  7284  riotaeqimp  7389  ov6g  7568  tfindsg  7847  findsg  7887  suppimacnv  8156  suppssOLD  8177  ectocld  8775  ecoptocl  8798  undifixp  8925  phplem3OLD  9216  f1dmvrnfibi  9333  f1vrnfibi  9334  updjud  9926  card1  9960  pr2neOLD  9997  prdom2  9998  sornom  10269  indpi  10899  ltlen  11312  eqlei  11321  squeeze0  12114  nn0ind-raph  12659  injresinjlem  13749  modmuladd  13875  modmuladdnn0  13877  hashf1rn  14309  hashrabsn1  14331  hash1snb  14376  hashgt12el  14379  hashgt12el2  14380  hashfzp1  14388  hash2prde  14428  hash2pwpr  14434  fi1uzind  14455  brfi1indALT  14458  lswlgt0cl  14516  wrd2ind  14670  pfxccatin12lem2  14678  pfxccatin12lem3  14679  cshweqrep  14768  cshwsexaOLD  14772  scshwfzeqfzo  14774  cshimadifsn  14777  cshimadifsn0  14778  2swrd2eqwrdeq  14901  wwlktovfo  14906  rennim  15183  absmod0  15247  modfsummods  15736  mod2eq1n2dvds  16287  m1expe  16314  m1expo  16315  m1exp1  16316  nn0o1gt2  16321  flodddiv4  16353  cncongr1  16601  ge2nprmge4  16635  m1dvdsndvds  16728  cshwrepswhash1  17033  initoeu2lem1  17961  istos  18368  mgmsscl  18563  mndinvmod  18652  smndex1n0mnd  18790  symgfvne  19243  symgfix2  19279  symgextf1  19284  symgfixelsi  19298  psgnsn  19383  odbezout  19421  cntzcmnss  19704  frgpnabllem1  19736  ringinvnzdiv  20107  psgndiflemB  21145  uvcendim  21394  mamufacex  21883  smatvscl  22018  mavmulsolcl  22045  mdetunilem8  22113  pm2mpfo  22308  chpscmat  22336  chmaidscmat  22342  chfacfscmulgsum  22354  chfacfpmmulgsum  22358  txcn  23122  qtopeu  23212  reeff1o  25951  relogbcxpb  26282  logbgcd1irr  26289  zabsle1  26789  2lgslem1c  26886  2lgsoddprmlem3  26907  2sq2  26926  2sqreultlem  26940  2sqreunnltlem  26943  2sqreulem3  26946  pntrlog2bndlem5  27074  upgrpredgv  28389  usgredg2vlem2  28473  ushgredgedg  28476  ushgredgedgloop  28478  uhgrspan1  28550  nb3grprlem1  28627  uvtxnbgrb  28648  cusgrsize2inds  28700  1egrvtxdg0  28758  uspgrloopvtxel  28763  finsumvtxdg2size  28797  rusgrpropnb  28830  ifpsnprss  28870  upgrwlkvtxedg  28892  uspgr2wlkeq  28893  wlkp1lem5  28924  wlkp1  28928  usgr2pth  29011  uspgrn2crct  29052  iswwlksnon  29097  wlkiswwlks1  29111  wlkiswwlks2lem3  29115  wwlksnextbi  29138  wwlksnredwwlkn0  29140  wwlksnextwrd  29141  wwlksnextsurj  29144  wwlksnextprop  29156  wspn0  29168  umgr2adedgwlkonALT  29191  umgr2adedgspth  29192  umgr2wlkon  29194  elwwlks2ons3  29199  elwwlks2on  29203  clwlkclwwlklem2a4  29240  clwlkclwwlklem2a  29241  clwlkclwwlkf1lem3  29249  clwwlkfo  29293  eleclclwwlknlem2  29304  erclwwlkntr  29314  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  0wlkonlem1  29361  upgr1wlkdlem1  29388  1pthon2v  29396  upgr3v3e3cycl  29423  uhgr3cyclexlem  29424  upgr4cycl4dv4e  29428  eupth2lem3lem3  29473  eupth2lem3lem4  29474  1to2vfriswmgr  29522  frgrncvvdeqlem6  29547  frgrncvvdeqlem8  29549  frgrncvvdeqlem9  29550  frgrwopreglem2  29556  2clwwlk2clwwlk  29593  extwwlkfab  29595  numclwwlk1lem2f1  29600  numclwwlkovh  29616  numclwwlk2lem1  29619  numclwlk2lem2f  29620  cdj1i  31674  brabgaf  31825  br8d  31827  sgn3da  33529  spthcycl  34109  goalrlem  34376  goalr  34377  fmlasucdisj  34379  satffunlem  34381  satffunlem1lem1  34382  satffunlem1lem2  34383  satffunlem2lem1  34384  satffunlem2lem2  34386  mthmb  34561  br8  34715  br4  34717  bj-snsetex  35833  bj-snglc  35839  copsex2d  36009  poimirlem20  36497  poimirlem26  36503  poimirlem27  36504  mblfinlem3  36516  mblfinlem4  36517  itg2addnclem  36528  indexdom  36591  ismgmOLD  36707  rngodm1dm2  36789  rngomndo  36792  rngoueqz  36797  zerdivemp1x  36804  opcon3b  38055  ps-1  38337  3atlem5  38347  4atex  38936  selvvvval  41155  prjspvs  41349  iscard4  42270  pr2cv  42285  pm13.192  43155  iotavalsb  43178  fourierdlem32  44842  fourierdlem49  44858  fourierdlem64  44873  elprneb  45726  fveqvfvv  45737  funressnfv  45740  f1cof1b  45772  nvelim  45818  afvpcfv0  45841  afv0nbfvbi  45846  fnbrafvb  45849  tz6.12-afv  45868  afvco2  45871  ndmaovg  45879  afv2orxorb  45923  tz6.12-afv2  45935  tz6.12i-afv2  45938  f1oresf1o2  45986  fzoopth  46022  elsetpreimafvbi  46046  imasetpreimafvbijlemfo  46060  iccpartiltu  46077  fargshiftfv  46094  fargshiftf  46095  lswn0  46099  prsprel  46142  reupr  46177  2exopprim  46180  fmtnorec2lem  46197  2pwp1prm  46244  lighneallem2  46261  lighneallem3  46262  proththd  46269  nn0o1gt2ALTV  46349  evenltle  46372  sbgoldbwt  46432  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  isomushgr  46481  isomuspgrlem1  46482  uspgropssxp  46509  lmod0rng  46629  lidldomn1  46777  zlidlring  46780  rngcinv  46833  rngcinvALTV  46845  ztprmneprm  46977  lincext3  47091  zlmodzxznm  47132  suppdm  47145  elfzolborelfzop1  47154  nn0sumshdiglemB  47260  itcovalsucov  47308  lines  47371  rrx2vlinest  47381  line2xlem  47393  itschlc0yqe  47400  itsclquadeu  47417