Theorem eqeq1d 2186

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

Hypothesis

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

Assertion

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

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 |- ( ph -> A = B )
2		eqeq1 2184	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A = C <-> B = C ) )

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:  rspcedeq1vd  2852  sbceq2g  3081  csbhypf  3097  csbiebt  3098  csbiebg  3101  dfss4st  3370  disjssun  3488  sneqrg  3764  preq12b  3772  preq12bg  3775  disji2  3998  iin0r  4171  opthg  4240  opeqsn  4254  unisucg  4416  opthreg  4557  tfisi  4588  dmsnopg  5102  relcoi1  5162  iotaeq  5188  iotabi  5189  fneq1  5306  fnun  5324  fnresdisj  5328  fnimadisj  5338  fnimaeq0  5339  sbcfng  5365  foeq1  5436  foco  5450  fveqeq2d  5525  fvelimab  5575  fvun1  5585  fvmptdv2  5608  fneqeql  5627  dffo3  5666  fvsng  5715  fconstfvm  5737  eufnfv  5750  f1veqaeq  5773  dff13f  5774  f1elima  5777  foeqcnvco  5794  f1eqcocnv  5795  acexmidlemab  5872  ovanraleqv  5902  eloprabga  5965  ovmpodv2  6011  ovi3  6014  ovelimab  6028  caovcang  6039  caovcan  6042  caovimo  6071  suppssfv  6082  suppssov1  6083  caofinvl  6108  op1stg  6154  op2ndg  6155  eqop  6181  reldm  6190  xporderlem  6235  tposfo2  6271  frec0g  6401  freccllem  6406  frecfcllem  6408  frecsuclem  6410  frecsuc  6411  nnm0r  6483  nnmord  6521  nnaordex  6532  nnawordex  6533  ereq1  6545  eqerlem  6569  mapsn  6693  endisj  6827  xpf1o  6847  mapxpen  6851  fidifsnen  6873  supelti  7004  updjudhcoinlf  7082  updjudhcoinrg  7083  updjud  7084  omp1eomlem  7096  difinfsnlem  7101  nnnninfeq  7129  enomnilem  7139  finomni  7141  exmidomni  7143  fodjuomnilemres  7149  fodjuomni  7150  ismkvnex  7156  mkvprop  7159  fodjumkvlemres  7160  enmkvlem  7162  enwomnilem  7170  nninfdcinf  7172  nninfwlporlem  7174  nninfwlpoimlemginf  7177  pm54.43  7192  exmidfodomrlemrALT  7205  cc2lem  7268  addnidpig  7338  ltexpi  7339  dfplpq2  7356  dfmpq2  7357  recexnq  7392  recmulnqg  7393  ltexnqq  7410  halfnqq  7412  enq0tr  7436  nqnq0pi  7440  addnnnq0  7451  addlocpr  7538  ltexprlemru  7614  ltexpri  7615  lteupri  7619  prplnqu  7622  recexpr  7640  addsrpr  7747  mulsrpr  7748  00sr  7771  negexsr  7774  recexgt0sr  7775  srpospr  7785  prsrriota  7790  caucvgsrlemfv  7793  map2psrprg  7807  elrealeu  7831  axrnegex  7881  axprecex  7882  rereceu  7891  recriota  7892  nntopi  7896  axcaucvglemval  7899  axcaucvglemcau  7900  cnegexlem1  8135  cnegex  8138  cnegex2  8139  subval  8152  subadd  8163  subadd2  8164  subsub23  8165  addsubeq4  8175  subcan2  8185  negcon1  8212  subcan  8215  addrsub  8331  ltadd2  8379  ltordlem  8442  recexre  8538  recexap  8613  muleqadd  8628  receuap  8629  divvalap  8634  divmulap  8635  rec11ap  8670  rerecapb  8803  zdiv  9344  uzin  9563  xaddval  9848  xnn0xadd0  9870  xnegdi  9871  xltadd1  9879  icc0r  9929  fznlem  10044  fseq1m1p1  10098  1fv  10142  fzon  10169  fvinim0ffz  10244  ioo0  10263  ico0  10265  ioc0  10266  flqbi  10293  divfl0  10299  modq0  10332  modqmuladdnn0  10371  addmodlteq  10401  frecuzrdgtcl  10415  frecuzrdgfunlem  10422  seq3f1olemstep  10504  seq3f1olemp  10505  seq3id  10511  seq3z  10514  qsqeqor  10634  mulreap  10876  rennim  11014  resqrexlemex  11037  rsqrmo  11039  resqrtcl  11041  rersqrtthlem  11042  sqrtsq2  11055  isumss  11402  fsum00  11473  telfsumo  11477  pwm1geoserap1  11519  prodssdc  11600  absefib  11781  efieq1re  11782  divides  11799  dvdsval2  11800  nndivides  11807  dvds0lem  11811  dvds1lem  11812  dvds2lem  11813  negdvdsb  11817  muldvds1  11826  muldvds2  11827  dvdscmulr  11830  dvdsmulcr  11831  dvdstr  11838  dvdsabseq  11856  divconjdvds  11858  odd2np1lem  11880  odd2np1  11881  even2n  11882  oddm1even  11883  2tp1odd  11892  opeo  11905  omeo  11906  m1exp1  11909  divalgb  11933  gcdaddm  11988  gcdabs1  11993  bezout  12015  gcdmultiple  12024  gcdmultiplez  12025  rplpwr  12031  rppwr  12032  alginv  12050  algcvga  12054  algfx  12055  eucalgval2  12056  coprmdvds  12095  qredeq  12099  qredeu  12100  divgcdcoprm0  12104  divgcdcoprmex  12105  cncongr1  12106  rpexp  12156  rpexp12i  12158  cncongrprm  12160  qnumdenbi  12195  phival  12216  phicl2  12217  dfphi2  12223  phiprmpw  12225  phimullem  12228  eulerthlem1  12230  eulerthlemfi  12231  eulerthlemrprm  12232  eulerthlemth  12235  eulerth  12236  fermltl  12237  hashgcdlem  12241  phisum  12243  odzval  12244  odzdvds  12248  reumodprminv  12256  modprm0  12257  nnnn0modprm0  12258  modprmn0modprm0  12259  coprimeprodsq  12260  coprimeprodsq2  12261  pythagtriplem2  12269  pythagtrip  12286  pceulem  12297  pcval  12299  pcqmul  12306  pcqcl  12309  pcabs  12328  pc2dvds  12332  pcaddlem  12341  pcadd  12342  pcmpt  12344  prmpwdvds  12356  pockthi  12359  ennnfonelemhf1o  12417  fvprif  12768  mgmidmo  12797  grpidvalg  12798  grpidpropdg  12799  ismgmid  12802  ismgmid2  12805  mgmidsssn0  12809  grprinvlem  12810  grpridd  12812  ismnddef  12825  sgrpidmndm  12827  ismndd  12844  mndpropd  12847  mndinvmod  12852  mnd1  12853  ismhm  12859  grpinvex  12893  isgrpd2  12903  isgrpd  12905  dfgrp2  12908  grpinveu  12917  grpinvval  12922  grplinv  12928  isgrpinv  12932  grplrinv  12933  grpidinv2  12934  grpidinv  12935  grplmulf1o  12950  grpsubeq0  12962  grpsubadd  12964  dfgrp3mlem  12974  dfgrp3m  12975  grp1  12982  mhmmnd  12986  ghmgrp  12988  mulgval  12992  mulgaddcom  13013  ablsubadd  13121  ablsubsub23  13134  dfur2g  13151  srgideu  13161  srgidmlem  13167  issrgid  13170  srgrz  13173  srglz  13174  srgisid  13175  srg1zr  13176  ringideu  13206  ringidmlem  13211  isringid  13214  ringid  13215  oppr0g  13257  oppr1g  13258  reldvdsrsrg  13267  dvdsrvald  13268  dvdsrmuld  13271  dvdsr01  13279  dvdsr02  13280  opprunitd  13285  crngunit  13286  unitinvinv  13299  dvreq1  13317  dvdsrpropdg  13322  lringuplu  13343  subrg1  13358  subrgdvds  13362  islmod  13387  islmodd  13389  lmodprop2d  13444  lss1d  13476  ntreq0  13772  ispsmet  13963  psmet0  13967  ismet  13984  isxmet  13985  xmeteq0  13999  metn0  14018  xmetres2  14019  xblss2ps  14044  xblss2  14045  xmseq0  14108  comet  14139  bdxmet  14141  cnmet  14170  ivthdec  14262  reeff1o  14334  ioocosf1o  14415  logbgcd1irr  14525  logbgcd1irraplemexp  14526  lgsval  14545  lgsdir  14576  lgsne0  14579  lgsprme0  14583  lgsdirnn0  14588  lgseisenlem2  14591  m1lgs  14592  2sqlem7  14608  2sqlem8  14610  2sqlem9  14611  bj-charfunbi  14703  pwle2  14889  subctctexmid  14891  peano4nninf  14896  nninfalllem1  14898  nninfsellemdc  14900  nninfsellemeq  14904  nninfsellemqall  14905  nninfsellemeqinf  14906  isomninnlem  14919  trilpolemlt1  14930  trirec0  14933  iswomninnlem  14938  iswomni0  14940  ismkvnnlem  14941  dceqnconst  14949  dcapnconst  14950