Theorem eqcoms 2747

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

Syntax hints:   → wi 4   = wceq 1539

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  gencbvex  3489  sbceq2a  3729  eqimss2  3979  uneqdifeq  4424  tppreq3  4696  ifpprsnss  4701  tpprceq3  4738  preqsnd  4790  elpr2elpr  4800  prproe  4838  copsex2t  5407  copsex2gOLD  5409  snopeqop  5421  opthhausdorff0  5433  relopabi  5734  cnvimassrndm  6060  cnveqb  6104  cnveq0  6105  unixpid  6191  reuop  6200  f0rn0  6668  fimadmfo  6706  f1ssf1  6757  tz6.12i  6809  fveqdmss  6965  fvcofneq  6978  funopsn  7029  f1ocnvfv  7159  f1ocnvfvb  7160  cbvfo  7170  riotaeqimp  7268  ov6g  7445  tfindsg  7716  findsg  7755  suppimacnv  7999  suppssOLD  8020  ectocld  8582  ecoptocl  8605  undifixp  8731  phplem3OLD  9011  f1dmvrnfibi  9112  f1vrnfibi  9113  updjud  9701  card1  9735  pr2ne  9770  prdom2  9771  sornom  10042  indpi  10672  ltlen  11085  eqlei  11094  squeeze0  11887  nn0ind-raph  12429  injresinjlem  13516  modmuladd  13642  modmuladdnn0  13644  hashf1rn  14076  hashrabsn1  14098  hash1snb  14143  hashgt12el  14146  hashgt12el2  14147  hashfzp1  14155  hash2prde  14193  hash2pwpr  14199  fi1uzind  14220  brfi1indALT  14223  lswlgt0cl  14281  wrd2ind  14445  pfxccatin12lem2  14453  pfxccatin12lem3  14454  cshweqrep  14543  cshwsexa  14546  scshwfzeqfzo  14548  cshimadifsn  14551  cshimadifsn0  14552  2swrd2eqwrdeq  14675  wwlktovfo  14682  rennim  14959  absmod0  15024  modfsummods  15514  mod2eq1n2dvds  16065  m1expe  16092  m1expo  16093  m1exp1  16094  nn0o1gt2  16099  flodddiv4  16131  cncongr1  16381  ge2nprmge4  16415  m1dvdsndvds  16508  cshwrepswhash1  16813  initoeu2lem1  17738  istos  18145  mgmsscl  18340  mndinvmod  18424  smndex1n0mnd  18560  symgfvne  18997  symgfix2  19033  symgextf1  19038  symgfixelsi  19052  psgnsn  19137  odbezout  19174  cntzcmnss  19451  frgpnabllem1  19483  ringinvnzdiv  19841  psgndiflemB  20814  uvcendim  21063  mamufacex  21547  smatvscl  21682  mavmulsolcl  21709  mdetunilem8  21777  pm2mpfo  21972  chpscmat  22000  chmaidscmat  22006  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  txcn  22786  qtopeu  22876  reeff1o  25615  relogbcxpb  25946  logbgcd1irr  25953  zabsle1  26453  2lgslem1c  26550  2lgsoddprmlem3  26571  2sq2  26590  2sqreultlem  26604  2sqreunnltlem  26607  2sqreulem3  26610  pntrlog2bndlem5  26738  upgrpredgv  27518  usgredg2vlem2  27602  ushgredgedg  27605  ushgredgedgloop  27607  uhgrspan1  27679  nb3grprlem1  27756  uvtxnbgrb  27777  cusgrsize2inds  27829  1egrvtxdg0  27887  uspgrloopvtxel  27892  finsumvtxdg2size  27926  rusgrpropnb  27959  ifpsnprss  27999  upgrwlkvtxedg  28021  uspgr2wlkeq  28022  wlkp1lem5  28054  wlkp1  28058  usgr2pth  28141  uspgrn2crct  28182  iswwlksnon  28227  wlkiswwlks1  28241  wlkiswwlks2lem3  28245  wwlksnextbi  28268  wwlksnredwwlkn0  28270  wwlksnextwrd  28271  wwlksnextsurj  28274  wwlksnextprop  28286  wspn0  28298  umgr2adedgwlkonALT  28321  umgr2adedgspth  28322  umgr2wlkon  28324  elwwlks2ons3  28329  elwwlks2on  28333  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlkf1lem3  28379  clwwlkfo  28423  eleclclwwlknlem2  28434  erclwwlkntr  28444  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  0wlkonlem1  28491  upgr1wlkdlem1  28518  1pthon2v  28526  upgr3v3e3cycl  28553  uhgr3cyclexlem  28554  upgr4cycl4dv4e  28558  eupth2lem3lem3  28603  eupth2lem3lem4  28604  1to2vfriswmgr  28652  frgrncvvdeqlem6  28677  frgrncvvdeqlem8  28679  frgrncvvdeqlem9  28680  frgrwopreglem2  28686  2clwwlk2clwwlk  28723  extwwlkfab  28725  numclwwlk1lem2f1  28730  numclwwlkovh  28746  numclwwlk2lem1  28749  numclwlk2lem2f  28750  cdj1i  30804  brabgaf  30957  br8d  30959  sgn3da  32517  spthcycl  33100  goalrlem  33367  goalr  33368  fmlasucdisj  33370  satffunlem  33372  satffunlem1lem1  33373  satffunlem1lem2  33374  satffunlem2lem1  33375  satffunlem2lem2  33377  mthmb  33552  br8  33732  br4  33734  bj-snsetex  35162  bj-snglc  35168  copsex2d  35319  poimirlem20  35806  poimirlem26  35812  poimirlem27  35813  mblfinlem3  35825  mblfinlem4  35826  itg2addnclem  35837  indexdom  35901  ismgmOLD  36017  rngodm1dm2  36099  rngomndo  36102  rngoueqz  36107  zerdivemp1x  36114  opcon3b  37217  ps-1  37498  3atlem5  37508  4atex  38097  prjspvs  40456  iscard4  41147  pr2cv  41162  pm13.192  42035  iotavalsb  42058  fourierdlem32  43687  fourierdlem49  43703  fourierdlem64  43718  elprneb  44534  fveqvfvv  44545  funressnfv  44548  f1cof1b  44580  nvelim  44626  afvpcfv0  44649  afv0nbfvbi  44654  fnbrafvb  44657  tz6.12-afv  44676  afvco2  44679  ndmaovg  44687  afv2orxorb  44731  tz6.12-afv2  44743  tz6.12i-afv2  44746  f1oresf1o2  44794  fzoopth  44830  elsetpreimafvbi  44854  imasetpreimafvbijlemfo  44868  iccpartiltu  44885  fargshiftfv  44902  fargshiftf  44903  lswn0  44907  prsprel  44950  reupr  44985  2exopprim  44988  fmtnorec2lem  45005  2pwp1prm  45052  lighneallem2  45069  lighneallem3  45070  proththd  45077  nn0o1gt2ALTV  45157  evenltle  45180  sbgoldbwt  45240  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  isomushgr  45289  isomuspgrlem1  45290  uspgropssxp  45317  lmod0rng  45437  lidldomn1  45490  zlidlring  45497  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  ztprmneprm  45694  lincext3  45808  zlmodzxznm  45849  suppdm  45862  elfzolborelfzop1  45871  nn0sumshdiglemB  45977  itcovalsucov  46025  lines  46088  rrx2vlinest  46098  line2xlem  46110  itschlc0yqe  46117  itsclquadeu  46134