Theorem eqeq2d 2152

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  eqtrd  2173  eq2tri  2200  rspcedeq2vd  2803  rspceeqv  2811  sbceq1g  3027  euabsn  3601  absneu  3603  preq12bg  3708  cbvopab  4007  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  cbvopab2v  4013  mpteq12f  4016  cbvmptf  4030  cbvmpt  4031  exmidsssn  4133  exmidsssnc  4134  opth  4167  eqvinop  4173  moop2  4181  euotd  4184  eusvnf  4382  reusv3i  4388  nlimsucg  4489  nn0suc  4526  opelxp  4577  elvvv  4610  relop  4697  elrnmpt1s  4797  elrnmpt1  4798  elsnres  4864  elxp4  5034  elxp5  5035  relresfld  5076  iotajust  5095  iota1  5110  iota2df  5120  funopg  5165  funcnvuni  5200  fun11iun  5396  funcocnv2  5400  nfvres  5462  ssimaex  5490  fvmptg  5505  fvmptdf  5516  fvopab6  5525  fmptco  5594  fsng  5601  foco2  5663  elabrex  5667  abrexco  5668  f1veqaeq  5678  dff13f  5679  f1ocnvfv  5688  f1ocnvfvb  5689  fcofo  5693  fliftfun  5705  fliftval  5709  f1oiso2  5736  riota5f  5762  oprabid  5811  rspceov  5821  dfoprab2  5826  mpoeq123dva  5840  mpoeq3dva  5843  cbvoprab1  5851  cbvoprab2  5852  cbvoprab12  5853  cbvmpox  5857  mpomptx  5870  ovmpos  5902  ovmpodf  5910  ovmpodv2  5912  ovi3  5915  ov6g  5916  fnrnov  5924  foov  5925  caovcang  5940  caovcan  5943  f1opw2  5984  opabex3d  6027  opabex3  6028  fo1st  6063  fo2nd  6064  elxp6  6075  op1steq  6085  dfoprab4f  6099  fmpox  6106  fnmpoovd  6120  df1st2  6124  df2nd2  6125  xporderlem  6136  cnvoprab  6139  f1od2  6140  brtpos2  6156  dftpos4  6168  tposfn2  6171  recseq  6211  tfr1onlemaccex  6253  tfrcllemaccex  6266  frecabcl  6304  frecsuc  6312  nna0r  6382  eqerlem  6468  qseq2  6486  ecelqsg  6490  snec  6498  qsinxp  6513  ecoptocl  6524  eroveu  6528  th3qlem1  6539  th3qlem2  6540  th3q  6542  mapsncnv  6597  elixpsn  6637  ixpsnf1o  6638  en1  6701  mapsnen  6713  xpsnen  6723  xpassen  6732  xpf1o  6746  mapen  6748  mapxpen  6750  fidifsnen  6772  ac6sfi  6800  undifdc  6820  djuf1olem  6946  djur  6962  updjud  6975  omp1eomlem  6987  0ct  7000  enumctlemm  7007  fodjuomnilemdc  7024  fodjuomni  7029  fodjumkv  7042  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  cc2lem  7098  dfplpq2  7186  dfmpq2  7187  enqbreq2  7189  enq0sym  7264  enq0ref  7265  enq0tr  7266  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  mulnnnq0  7282  nqnq0a  7286  nqnq0m  7287  nq0a0  7289  prarloclemcalc  7334  genipv  7341  genpassl  7356  genpassu  7357  addcomprg  7410  mulcomprg  7412  distrlem1prl  7414  distrlem1pru  7415  distrlem5prl  7418  distrlem5pru  7419  1idprl  7422  1idpru  7423  recexprlem1ssl  7465  recexprlem1ssu  7466  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  elreal  7660  axcnre  7713  axcaucvglemval  7729  negeu  7977  subeq0  8012  apreap  8373  apreim  8389  divmulap3  8461  diveqap0  8466  diveqap1  8489  nn0ind-raph  9192  elq  9441  zq  9445  elpq  9467  cnref1o  9469  iccf1o  9817  fzen  9854  fseq1m1p1  9906  fzm1  9911  modqmuladd  10170  modqmuladdnn0  10172  modfzo0difsn  10199  nn0ennn  10237  seq3id2  10313  bcval5  10541  fihashen1  10577  shftlem  10620  shftfvalg  10622  shftfval  10625  negfi  11031  xrmaxiflemcom  11050  xrnegiso  11063  xrnegcon1d  11065  sumeq2  11160  summodc  11184  fsum3  11188  fsum2dlemstep  11235  isumsplit  11292  mertenslemub  11335  mertensabs  11338  prodeq2w  11357  prodeq2  11358  prodmodc  11379  fprodseq  11384  moddvds  11538  dvdsnegb  11546  dvdsabseq  11581  dvdsmod  11596  odd2np1lem  11605  odd2np1  11606  opeo  11630  omeo  11631  divalglemnn  11651  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  bezoutlemnewy  11720  bezoutlema  11723  bezoutlemb  11724  bezoutlemex  11725  bezoutlemaz  11727  bezoutlembz  11728  eucalglt  11774  qredeq  11813  qredeu  11814  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  qnumdenbi  11906  hashgcdlem  11939  evenennn  11942  ennnfonelemim  11973  istopon  12219  eltg3  12265  restsn  12388  txuni2  12464  txopn  12473  upxp  12480  uptx  12482  txrest  12484  hmeoimaf1o  12522  xmettxlem  12717  xmettx  12718  bj-nn0suc0  13319  bj-inf2vnlem1  13339  bj-nn0sucALT  13347  pwle2  13366  iooref1o  13426