Theorem eqeq1d 2205

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 2203	. 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 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  rspcedeq1vd  2877  sbceq2g  3106  csbhypf  3123  csbiebt  3124  csbiebg  3127  dfss4st  3397  disjssun  3515  sneqrg  3793  preq12b  3801  preq12bg  3804  disji2  4027  iin0r  4203  opthg  4272  opeqsn  4286  unisucg  4450  opthreg  4593  tfisi  4624  dmsnopg  5142  relcoi1  5202  iotaeq  5228  iotabi  5229  fneq1  5347  fnun  5367  fnresdisj  5371  fnimadisj  5381  fnimaeq0  5382  sbcfng  5408  foeq1  5479  foco  5494  fveqeq2d  5569  fvelimab  5620  fvun1  5630  fvmptdv2  5654  fneqeql  5673  dffo3  5712  fvsng  5761  fconstfvm  5783  eufnfv  5796  f1veqaeq  5819  dff13f  5820  f1elima  5823  foeqcnvco  5840  f1eqcocnv  5841  acexmidlemab  5919  ovanraleqv  5949  eloprabga  6013  ovmpodv2  6060  ovi3  6064  ovelimab  6078  caovcang  6089  caovcan  6092  caovimo  6121  suppssfv  6135  suppssov1  6136  caofinvl  6165  caofid1  6168  caofid2  6169  uchoice  6204  op1stg  6217  op2ndg  6218  eqop  6244  reldm  6253  xporderlem  6298  tposfo2  6334  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnm0r  6546  nnmord  6584  nnaordex  6595  nnawordex  6596  ereq1  6608  eqerlem  6632  mapsn  6758  endisj  6892  pw2f1odclem  6904  xpf1o  6914  mapxpen  6918  fidifsnen  6940  supelti  7077  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  omp1eomlem  7169  difinfsnlem  7174  nnnninfeq  7203  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  fodjuomni  7224  ismkvnex  7230  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemginf  7251  pm54.43  7269  exmidfodomrlemrALT  7282  cc2lem  7349  addnidpig  7420  ltexpi  7421  dfplpq2  7438  dfmpq2  7439  recexnq  7474  recmulnqg  7475  ltexnqq  7492  halfnqq  7494  enq0tr  7518  nqnq0pi  7522  addnnnq0  7533  addlocpr  7620  ltexprlemru  7696  ltexpri  7697  lteupri  7701  prplnqu  7704  recexpr  7722  addsrpr  7829  mulsrpr  7830  00sr  7853  negexsr  7856  recexgt0sr  7857  srpospr  7867  prsrriota  7872  caucvgsrlemfv  7875  map2psrprg  7889  elrealeu  7913  axrnegex  7963  axprecex  7964  rereceu  7973  recriota  7974  nntopi  7978  axcaucvglemval  7981  axcaucvglemcau  7982  cnegexlem1  8218  cnegex  8221  cnegex2  8222  subval  8235  subadd  8246  subadd2  8247  subsub23  8248  addsubeq4  8258  subcan2  8268  negcon1  8295  subcan  8298  addrsub  8414  ltadd2  8463  ltordlem  8526  recexre  8622  recexap  8697  muleqadd  8712  receuap  8713  divvalap  8718  divmulap  8719  rec11ap  8754  rerecapb  8887  zdiv  9431  uzin  9651  xaddval  9937  xnn0xadd0  9959  xnegdi  9960  xltadd1  9968  icc0r  10018  fznlem  10133  fseq1m1p1  10187  1fv  10231  fzon  10259  fvinim0ffz  10334  ioo0  10366  ico0  10368  ioc0  10369  flqbi  10397  divfl0  10403  modq0  10438  modqmuladdnn0  10477  addmodlteq  10507  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  seq3f1olemstep  10623  seq3f1olemp  10624  seq3id  10634  seq3z  10637  qsqeqor  10759  mulreap  11046  rennim  11184  resqrexlemex  11207  rsqrmo  11209  resqrtcl  11211  rersqrtthlem  11212  sqrtsq2  11225  isumss  11573  fsum00  11644  telfsumo  11648  pwm1geoserap1  11690  prodssdc  11771  absefib  11953  efieq1re  11954  divides  11971  dvdsval2  11972  nndivides  11979  dvds0lem  11983  dvds1lem  11984  dvds2lem  11985  negdvdsb  11989  muldvds1  11998  muldvds2  11999  dvdscmulr  12002  dvdsmulcr  12003  dvdstr  12010  dvdsabseq  12029  divconjdvds  12031  odd2np1lem  12054  odd2np1  12055  even2n  12056  oddm1even  12057  2tp1odd  12066  opeo  12079  omeo  12080  m1exp1  12083  divalgb  12107  gcdaddm  12176  gcdabs1  12181  bezout  12203  gcdmultiple  12212  gcdmultiplez  12213  rplpwr  12219  rppwr  12220  nninfctlemfo  12232  alginv  12240  algcvga  12244  algfx  12245  eucalgval2  12246  coprmdvds  12285  qredeq  12289  qredeu  12290  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  rpexp  12346  rpexp12i  12348  cncongrprm  12350  qnumdenbi  12385  phival  12406  phicl2  12407  dfphi2  12413  phiprmpw  12415  phimullem  12418  eulerthlem1  12420  eulerthlemfi  12421  eulerthlemrprm  12422  eulerthlemth  12425  eulerth  12426  fermltl  12427  hashgcdlem  12431  phisum  12434  odzval  12435  odzdvds  12439  reumodprminv  12447  modprm0  12448  nnnn0modprm0  12449  modprmn0modprm0  12450  coprimeprodsq  12451  coprimeprodsq2  12452  pythagtriplem2  12460  pythagtrip  12477  pceulem  12488  pcval  12490  pcqmul  12497  pcqcl  12500  pcabs  12520  pc2dvds  12524  pcaddlem  12533  pcadd  12534  pcmpt  12537  prmpwdvds  12549  pockthi  12552  4sqlem12  12596  ennnfonelemhf1o  12655  fvprif  13045  mgmidmo  13074  grpidvalg  13075  grpidpropdg  13076  ismgmid  13079  ismgmid2  13082  mgmidsssn0  13086  grpinvalem  13087  grprida  13089  igsumvalx  13091  gsumress  13097  ismnddef  13120  sgrpidmndm  13122  ismndd  13139  mndpropd  13142  mndinvmod  13147  mnd1  13157  ismhm  13163  gsumvallem2  13195  grpinvex  13212  isgrpd2  13223  isgrpd  13225  dfgrp2  13229  grpinveu  13240  grpinvval  13245  grplinv  13252  isgrpinv  13256  grplrinv  13259  grpidinv2  13260  grpidinv  13261  grplmulf1o  13276  grpsubeq0  13288  grpsubadd  13290  dfgrp3mlem  13300  dfgrp3m  13301  grp1  13308  imasgrp2  13316  qusgrp2  13319  mhmmnd  13322  ghmgrp  13324  mulgval  13328  mulgaddcom  13352  eqg0el  13435  ghmeqker  13477  ghmf1  13479  conjnmzb  13486  ablsubadd  13518  ablsubsub23  13531  rngmneg1  13579  rngmneg2  13580  dfur2g  13594  srgideu  13604  srgidmlem  13610  issrgid  13613  srgrz  13616  srglz  13617  srgisid  13618  srg1zr  13619  ringideu  13649  ringidmlem  13654  isringid  13657  ringid  13658  qusring2  13698  oppr0g  13713  oppr1g  13714  reldvdsrsrg  13724  dvdsrvald  13725  dvdsrmuld  13728  dvdsr01  13736  dvdsr02  13737  opprunitd  13742  crngunit  13743  unitinvinv  13756  dvreq1  13774  dvdsrpropdg  13779  rhmdvdsr  13807  lringuplu  13828  subrg1  13863  subrgdvds  13867  isrrg  13895  rrgeq0i  13896  rrgeq0  13897  domneq0  13904  islmod  13923  islmodd  13925  lmodprop2d  13980  lss1d  14015  cnfldui  14221  znval  14268  znidom  14289  znunit  14291  znrrg  14292  ntreq0  14452  ispsmet  14643  psmet0  14647  ismet  14664  isxmet  14665  xmeteq0  14679  metn0  14698  xmetres2  14699  xblss2ps  14724  xblss2  14725  xmseq0  14788  comet  14819  bdxmet  14821  cnmet  14850  ivthdec  14964  ivthreinc  14965  elply2  15055  reeff1o  15093  ioocosf1o  15174  logbgcd1irr  15287  logbgcd1irraplemexp  15288  mpodvdsmulf1o  15310  lgsval  15329  lgsdir  15360  lgsne0  15363  lgsprme0  15367  lgsdirnn0  15372  gausslemma2dlem0c  15376  gausslemma2dlem0i  15382  gausslemma2dlem7  15393  gausslemma2d  15394  lgseisenlem2  15396  lgseisenlem3  15397  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  lgsquad3  15409  m1lgs  15410  2lgs  15429  2sqlem7  15446  2sqlem8  15448  2sqlem9  15449  bj-charfunbi  15541  2omap  15726  pwle2  15729  subctctexmid  15731  peano4nninf  15737  nninfalllem1  15739  nninfsellemdc  15741  nninfsellemeq  15745  nninfsellemqall  15746  nninfsellemeqinf  15747  isomninnlem  15761  trilpolemlt1  15772  trirec0  15775  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  dceqnconst  15791  dcapnconst  15792