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  2851  rspceeqv  2859  sbceq1g  3077  euabsn  3662  absneu  3664  preq12bg  3773  cbvopab  4074  cbvopab1  4076  cbvopab2  4077  cbvopab1s  4078  cbvopab2v  4080  mpteq12f  4083  cbvmptf  4097  cbvmpt  4098  exmidsssn  4202  exmidsssnc  4203  opth  4237  eqvinop  4243  moop2  4251  euotd  4254  eusvnf  4453  reusv3i  4459  nlimsucg  4565  nn0suc  4603  opelxp  4656  elvvv  4689  relop  4777  elrnmpt1s  4877  elrnmpt1  4878  elsnres  4944  elxp4  5116  elxp5  5117  relresfld  5158  iotajust  5177  iota1  5192  iota2df  5202  funopg  5250  funcnvuni  5285  fun11iun  5482  funcocnv2  5486  nfvres  5548  ssimaex  5577  fvmptg  5592  fvmptdf  5603  fvopab6  5612  fnmptfvd  5620  fmptco  5682  fsng  5689  foco2  5754  elabrex  5758  abrexco  5759  f1veqaeq  5769  dff13f  5770  f1ocnvfv  5779  f1ocnvfvb  5780  fcofo  5784  fliftfun  5796  fliftval  5800  f1oiso2  5827  riota5f  5854  oprabid  5906  rspceov  5916  dfoprab2  5921  mpoeq123dva  5935  mpoeq3dva  5938  cbvoprab1  5946  cbvoprab2  5947  cbvoprab12  5948  cbvmpox  5952  mpomptx  5965  ovmpos  5997  ovmpodf  6005  ovmpodv2  6007  ovi3  6010  ov6g  6011  fnrnov  6019  foov  6020  caovcang  6035  caovcan  6038  f1opw2  6076  opabex3d  6121  opabex3  6122  fo1st  6157  fo2nd  6158  elxp6  6169  op1steq  6179  dfoprab4f  6193  fmpox  6200  fnmpoovd  6215  df1st2  6219  df2nd2  6220  xporderlem  6231  cnvoprab  6234  f1od2  6235  brtpos2  6251  dftpos4  6263  tposfn2  6266  recseq  6306  tfr1onlemaccex  6348  tfrcllemaccex  6361  frecabcl  6399  frecsuc  6407  nna0r  6478  eqerlem  6565  qseq2  6583  ecelqsg  6587  snec  6595  qsinxp  6610  ecoptocl  6621  eroveu  6625  th3qlem1  6636  th3qlem2  6637  th3q  6639  mapsncnv  6694  elixpsn  6734  ixpsnf1o  6735  en1  6798  mapsnen  6810  xpsnen  6820  xpassen  6829  xpf1o  6843  mapen  6845  mapxpen  6847  fidifsnen  6869  ac6sfi  6897  undifdc  6922  djuf1olem  7051  djur  7067  updjud  7080  omp1eomlem  7092  0ct  7105  enumctlemm  7112  fodjuomnilemdc  7141  fodjuomni  7146  fodjumkv  7157  nninfwlporlemd  7169  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  cc2lem  7264  dfplpq2  7352  dfmpq2  7353  enqbreq2  7355  enq0sym  7430  enq0ref  7431  enq0tr  7432  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  mulnnnq0  7448  nqnq0a  7452  nqnq0m  7453  nq0a0  7455  prarloclemcalc  7500  genipv  7507  genpassl  7522  genpassu  7523  addcomprg  7576  mulcomprg  7578  distrlem1prl  7580  distrlem1pru  7581  distrlem5prl  7584  distrlem5pru  7585  1idprl  7588  1idpru  7589  recexprlem1ssl  7631  recexprlem1ssu  7632  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  elreal  7826  axcnre  7879  axcaucvglemval  7895  negeu  8147  subeq0  8182  apreap  8543  apreim  8559  divmulap3  8633  diveqap0  8638  diveqap1  8661  nn0ind-raph  9369  elq  9621  zq  9625  elpq  9647  cnref1o  9649  iccf1o  10003  fzen  10042  fseq1m1p1  10094  fzm1  10099  modqmuladd  10365  modqmuladdnn0  10367  modfzo0difsn  10394  nn0ennn  10432  seq3id2  10508  qsqeqor  10630  bcval5  10742  fihashen1  10778  shftlem  10824  shftfvalg  10826  shftfval  10829  negfi  11235  xrmaxiflemcom  11256  xrnegiso  11269  xrnegcon1d  11271  sumeq2  11366  summodc  11390  fsum3  11394  fsum2dlemstep  11441  isumsplit  11498  mertenslemub  11541  mertensabs  11544  prodeq2w  11563  prodeq2  11564  prodmodc  11585  fprodseq  11590  fprod2dlemstep  11629  moddvds  11805  modm1div  11806  dvdsnegb  11814  dvdsabseq  11852  dvdsmod  11867  odd2np1lem  11876  odd2np1  11877  opeo  11901  omeo  11902  divalglemnn  11922  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  bezoutlemnewy  11996  bezoutlema  11999  bezoutlemb  12000  bezoutlemex  12001  bezoutlemaz  12003  bezoutlembz  12004  eucalglt  12056  qredeq  12095  qredeu  12096  divgcdcoprm0  12100  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  qnumdenbi  12191  hashgcdlem  12237  coprimeprodsq2  12257  pythagtriplem18  12280  pythagtriplem19  12281  pceu  12294  pcval  12295  pczpre  12296  pcdiv  12301  dvdsprmpweq  12333  dvdsprmpweqnn  12334  difsqpwdvds  12336  pcmpt  12340  pcfac  12347  oddprmdvds  12351  4sqlem2  12386  4sqlem3  12387  4sqlem4  12389  evenennn  12393  ennnfonelemim  12424  ptex  12712  intopsn  12785  ismnddef  12818  sgrpidmndm  12820  mndpfo  12838  grpid  12911  grpidrcan  12934  grpidlcan  12935  grplactcnv  12971  srgpcomp  13171  ringadd2  13208  islmod  13379  istopon  13483  eltg3  13527  restsn  13650  txuni2  13726  txopn  13735  upxp  13742  uptx  13744  txrest  13746  hmeoimaf1o  13784  xmettxlem  13979  xmettx  13980  lgslem1  14371  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem2  14421  2lgsoddprmlem2  14424  2sqlem2  14432  2sqlem8  14440  2sqlem9  14441  bj-nn0suc0  14672  bj-inf2vnlem1  14692  bj-nn0sucALT  14700  pwle2  14718  iooref1o  14752