Theorem eqeq2d 2189

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 2187	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C = A <-> C = B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqtrd  2210  eq2tri  2237  rspcedeq2vd  2853  rspceeqv  2861  sbceq1g  3079  euabsn  3664  absneu  3666  preq12bg  3775  cbvopab  4076  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  cbvopab2v  4082  mpteq12f  4085  cbvmptf  4099  cbvmpt  4100  exmidsssn  4204  exmidsssnc  4205  opth  4239  eqvinop  4245  moop2  4253  euotd  4256  eusvnf  4455  reusv3i  4461  nlimsucg  4567  nn0suc  4605  opelxp  4658  elvvv  4691  relop  4779  elrnmpt1s  4879  elrnmpt1  4880  elsnres  4946  elxp4  5118  elxp5  5119  relresfld  5160  iotajust  5179  iota1  5194  iota2df  5204  funopg  5252  funcnvuni  5287  fun11iun  5484  funcocnv2  5488  nfvres  5550  ssimaex  5580  fvmptg  5595  fvmptdf  5606  fvopab6  5615  fnmptfvd  5623  fmptco  5685  fsng  5692  foco2  5757  elabrex  5761  elabrexg  5762  abrexco  5763  f1veqaeq  5773  dff13f  5774  f1ocnvfv  5783  f1ocnvfvb  5784  fcofo  5788  fliftfun  5800  fliftval  5804  f1oiso2  5831  riota5f  5858  oprabid  5910  rspceov  5920  dfoprab2  5925  mpoeq123dva  5939  mpoeq3dva  5942  cbvoprab1  5950  cbvoprab2  5951  cbvoprab12  5952  cbvmpox  5956  mpomptx  5969  ovmpos  6001  ovmpodf  6009  ovmpodv2  6011  ovi3  6014  ov6g  6015  fnrnov  6023  foov  6024  caovcang  6039  caovcan  6042  f1opw2  6080  opabex3d  6125  opabex3  6126  fo1st  6161  fo2nd  6162  elxp6  6173  op1steq  6183  dfoprab4f  6197  fmpox  6204  fnmpoovd  6219  df1st2  6223  df2nd2  6224  xporderlem  6235  cnvoprab  6238  f1od2  6239  brtpos2  6255  dftpos4  6267  tposfn2  6270  recseq  6310  tfr1onlemaccex  6352  tfrcllemaccex  6365  frecabcl  6403  frecsuc  6411  nna0r  6482  eqerlem  6569  qseq2  6587  ecelqsg  6591  snec  6599  qsinxp  6614  ecoptocl  6625  eroveu  6629  th3qlem1  6640  th3qlem2  6641  th3q  6643  mapsncnv  6698  elixpsn  6738  ixpsnf1o  6739  en1  6802  mapsnen  6814  xpsnen  6824  xpassen  6833  xpf1o  6847  mapen  6849  mapxpen  6851  fidifsnen  6873  ac6sfi  6901  undifdc  6926  djuf1olem  7055  djur  7071  updjud  7084  omp1eomlem  7096  0ct  7109  enumctlemm  7116  fodjuomnilemdc  7145  fodjuomni  7150  fodjumkv  7161  nninfwlporlemd  7173  exmidfodomrlemeldju  7201  exmidfodomrlemreseldju  7202  cc2lem  7268  dfplpq2  7356  dfmpq2  7357  enqbreq2  7359  enq0sym  7434  enq0ref  7435  enq0tr  7436  addnq0mo  7449  mulnq0mo  7450  addnnnq0  7451  mulnnnq0  7452  nqnq0a  7456  nqnq0m  7457  nq0a0  7459  prarloclemcalc  7504  genipv  7511  genpassl  7526  genpassu  7527  addcomprg  7580  mulcomprg  7582  distrlem1prl  7584  distrlem1pru  7585  distrlem5prl  7588  distrlem5pru  7589  1idprl  7592  1idpru  7593  recexprlem1ssl  7635  recexprlem1ssu  7636  addsrmo  7745  mulsrmo  7746  addsrpr  7747  mulsrpr  7748  elreal  7830  axcnre  7883  axcaucvglemval  7899  negeu  8151  subeq0  8186  apreap  8547  apreim  8563  divmulap3  8637  diveqap0  8642  diveqap1  8665  nn0ind-raph  9373  elq  9625  zq  9629  elpq  9651  cnref1o  9653  iccf1o  10007  fzen  10046  fseq1m1p1  10098  fzm1  10103  modqmuladd  10369  modqmuladdnn0  10371  modfzo0difsn  10398  nn0ennn  10436  seq3id2  10512  qsqeqor  10634  bcval5  10746  fihashen1  10782  shftlem  10828  shftfvalg  10830  shftfval  10833  negfi  11239  xrmaxiflemcom  11260  xrnegiso  11273  xrnegcon1d  11275  sumeq2  11370  summodc  11394  fsum3  11398  fsum2dlemstep  11445  isumsplit  11502  mertenslemub  11545  mertensabs  11548  prodeq2w  11567  prodeq2  11568  prodmodc  11589  fprodseq  11594  fprod2dlemstep  11633  moddvds  11809  modm1div  11810  dvdsnegb  11818  dvdsabseq  11856  dvdsmod  11871  odd2np1lem  11880  odd2np1  11881  opeo  11905  omeo  11906  divalglemnn  11926  divalglemeunn  11929  divalglemex  11930  divalglemeuneg  11931  bezoutlemnewy  12000  bezoutlema  12003  bezoutlemb  12004  bezoutlemex  12005  bezoutlemaz  12007  bezoutlembz  12008  eucalglt  12060  qredeq  12099  qredeu  12100  divgcdcoprm0  12104  divgcdcoprmex  12105  cncongr1  12106  cncongr2  12107  qnumdenbi  12195  hashgcdlem  12241  coprimeprodsq2  12261  pythagtriplem18  12284  pythagtriplem19  12285  pceu  12298  pcval  12299  pczpre  12300  pcdiv  12305  dvdsprmpweq  12337  dvdsprmpweqnn  12338  difsqpwdvds  12340  pcmpt  12344  pcfac  12351  oddprmdvds  12355  4sqlem2  12390  4sqlem3  12391  4sqlem4  12393  evenennn  12397  ennnfonelemim  12428  ptex  12719  intopsn  12793  ismnddef  12826  sgrpidmndm  12828  mndpfo  12846  grpid  12919  grpidrcan  12942  grpidlcan  12943  grplactcnv  12979  srgpcomp  13184  ringadd2  13221  islmod  13392  lss1d  13481  istopon  13674  eltg3  13718  restsn  13841  txuni2  13917  txopn  13926  upxp  13933  uptx  13935  txrest  13937  hmeoimaf1o  13975  xmettxlem  14170  xmettx  14171  lgslem1  14562  lgsdirnn0  14609  lgsdinn0  14610  lgseisenlem2  14612  2lgsoddprmlem2  14615  2sqlem2  14623  2sqlem8  14631  2sqlem9  14632  bj-nn0suc0  14863  bj-inf2vnlem1  14883  bj-nn0sucALT  14891  pwle2  14910  iooref1o  14944