Theorem eqeq2d 2250

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eqeq2d	|- ( ph -> ( C = A <-> C = B ) )

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 |- ( ph -> A = B )
2		eqeq2 2248	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C = A <-> C = B ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtrd  2271  eq2tri  2298  rspcedeq2vd  2940  rspceeqv  2948  sbceq1g  3167  ifeqeqxdc  3687  euabsn  3781  absneu  3783  ifpprsnssdc  3820  preq12bg  3898  cbvopab  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab2v  4209  mpteq12f  4212  cbvmptf  4227  cbvmpt  4228  exmidsssn  4341  exmidsssnc  4342  opth  4379  eqvinop  4385  moop2  4394  euotd  4397  eusvnf  4601  reusv3i  4607  nlimsucg  4715  nn0suc  4753  opelxp  4806  elvvv  4840  relop  4932  elrnmpt1s  5034  elrnmpt1  5035  elsnres  5102  elxp4  5278  elxp5  5279  relresfld  5320  iotajust  5339  iota1  5355  iota2df  5366  funopg  5414  funcnvuni  5453  fun11iun  5663  funcocnv2  5667  nfvres  5735  ssimaex  5767  fvmptg  5784  fvmptdf  5796  fvopab6  5808  fnmptfvd  5816  fmptco  5877  fsng  5884  fsn2g  5886  funopsn  5894  dfimafnf  5958  foco2  5962  elabrex  5966  elabrexg  5967  abrexco  5968  f1veqaeq  5978  dff13f  5979  f1ocnvfv  5988  f1ocnvfvb  5989  fcofo  5993  fliftfun  6005  fliftval  6009  f1oiso2  6036  riotaeqimp  6066  riota5f  6068  oprabid  6120  rspceov  6131  dfoprab2  6138  mpoeq123dva  6152  mpoeq3dva  6155  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvmpox  6169  mpomptx  6182  ovmpos  6215  ovmpodf  6223  ovmpodv2  6225  ovi3  6229  ov6g  6230  fnrnov  6238  foov  6239  caovcang  6254  caovcan  6257  f1opw2  6299  opabex3d  6354  opabex3  6355  fo1st  6395  fo2nd  6396  elxp6  6407  op1steq  6417  dfoprab4f  6431  fmpox  6440  fnmpoovd  6455  df1st2  6459  df2nd2  6460  xporderlem  6471  cnvoprab  6474  f1od2  6475  brtpos2  6527  dftpos4  6539  tposfn2  6542  recseq  6582  tfr1onlemaccex  6624  tfrcllemaccex  6637  frecabcl  6675  frecsuc  6683  nna0r  6756  eqerlem  6843  qseq2  6863  ecelqsg  6867  snec  6875  qsinxp  6890  ecoptocl  6901  eroveu  6905  th3qlem1  6916  th3qlem2  6917  th3q  6919  mapsncnv  6983  elixpsn  7023  ixpsnf1o  7024  en1  7092  mapsnend  7105  mapsnen  7106  en2  7118  xpsnen  7125  xpassen  7134  pw2f1odclem  7140  xpf1o  7150  mapen  7152  mapxpen  7154  mapunen  7157  fidifsnen  7178  ac6sfi  7208  undifdc  7237  djuf1olem  7399  djur  7415  updjud  7428  omp1eomlem  7440  0ct  7453  enumctlemm  7460  fodjuomnilemdc  7490  fodjuomni  7495  fodjumkv  7506  nninfwlporlemd  7518  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  cc2lem  7638  dfplpq2  7727  dfmpq2  7728  enqbreq2  7730  enq0sym  7805  enq0ref  7806  enq0tr  7807  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  nqnq0a  7827  nqnq0m  7828  nq0a0  7830  prarloclemcalc  7875  genipv  7882  genpassl  7897  genpassu  7898  addcomprg  7951  mulcomprg  7953  distrlem1prl  7955  distrlem1pru  7956  distrlem5prl  7959  distrlem5pru  7960  1idprl  7963  1idpru  7964  recexprlem1ssl  8006  recexprlem1ssu  8007  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  elreal  8201  axcnre  8254  axcaucvglemval  8270  negeu  8524  subeq0  8559  apreap  8923  apreim  8939  divmulap3  9015  diveqap0  9020  diveqap1  9043  nn0ind-raph  9773  elq  10037  zq  10041  elpq  10065  cnref1o  10067  iccf1o  10423  fzen  10463  fseq1m1p1  10518  fzm1  10523  modqmuladd  10823  modqmuladdnn0  10825  modfzo0difsn  10852  nn0ennn  10890  seqf1oglem1  10976  seq3id2  10983  qsqeqor  11107  bcval5  11222  fihashen1  11259  hashf1lem1  11306  wrdl1exs1  11418  wrdl1s1  11419  wrd2ind  11516  swrdccatin2d  11537  reuccatpfxs1lem  11539  shftlem  11602  shftfvalg  11604  shftfval  11607  negfi  12016  xrmaxiflemcom  12039  xrnegiso  12052  xrnegcon1d  12054  sumeq2  12149  summodc  12174  fsum3  12178  fsum2dlemstep  12225  isumsplit  12282  mertenslemub  12325  mertensabs  12328  prodeq2w  12347  prodeq2  12348  prodmodc  12369  fprodseq  12374  fprod2dlemstep  12413  moddvds  12590  modm1div  12591  dvdsnegb  12599  dvdsabseq  12638  dvdsmod  12653  odd2np1lem  12663  odd2np1  12664  opeo  12688  omeo  12689  divalglemnn  12709  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  bitsinv1lem  12752  bezoutlemnewy  12797  bezoutlema  12800  bezoutlemb  12801  bezoutlemex  12802  bezoutlemaz  12804  bezoutlembz  12805  eucalglt  12859  qredeq  12898  qredeu  12899  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  qnumdenbi  12996  nn0sqdcq  13012  hashgcdlem  13044  coprimeprodsq2  13065  pythagtriplem18  13088  pythagtriplem19  13089  pceu  13102  pcval  13103  pczpre  13104  pcdiv  13109  dvdsprmpweq  13142  dvdsprmpweqnn  13143  difsqpwdvds  13145  pcmpt  13150  pcfac  13157  oddprmdvds  13161  4sqlem2  13196  4sqlem3  13197  4sqlem4  13199  4sqlem12  13209  ballotfilemfc0  13289  ballotfilemfcc  13290  evenennn  13341  ennnfonelemim  13372  ptex  13676  intopsn  13745  gzsumvalx  13767  gzsumfzval  13769  gzsumress  13770  gzsumval2  13772  ismnddef  13789  sgrpidmndm  13791  mndpfo  13809  mhmex  13827  grpid  13902  grpidrcan  13928  grpidlcan  13929  grplactcnv  13965  isghm  14104  f1ghm0to0  14133  conjghm  14137  gsumvalfi  14241  srgpcomp  14400  ringadd2  14438  rrgval  14678  opprdomnbg  14691  islmod  14735  lss1d  14828  rspsn  14979  expghmap  15050  zndvds0  15093  znf1o  15094  psrbagconf1o  15177  mvrfval  15214  mvrval  15215  istopon  15256  eltg3  15300  restsn  15423  txuni2  15499  txopn  15508  upxp  15515  uptx  15517  txrest  15519  hmeoimaf1o  15557  xmettxlem  15752  xmettx  15753  elply2  15978  elplyr  15983  zprmlogbaplem3  16234  dvdsppwf1o  16300  mpodvdsmulf1o  16301  perfectlem2  16317  perfect  16318  lgslem1  16341  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  gausslemma2d  16410  lgseisenlem2  16412  lgsquadlem2  16419  2lgslem1b  16430  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2lgsoddprmlem2  16447  2sqlem2  16456  2sqlem8  16464  2sqlem9  16465  incistruhgr  16553  upgrex  16566  usgredg4  16678  usgredgreu  16679  uspgredg2vtxeu  16681  uspgredg2v  16684  usgredg2vlem2  16686  usgredg2v  16687  vtxdgfifival  16754  vtxdumgrfival  16761  1loopgrvd2fi  16768  wlk1walkdom  16822  upgriswlkdc  16823  eupth2lem3lem3fi  16933  eupth2fi  16942  bj-nn0suc0  17198  bj-inf2vnlem1  17218  bj-nn0sucALT  17226  pwle2  17250  iooref1o  17306  qdiff  17322