Theorem eqeq1d 2202

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 2200	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  rspcedeq1vd  2874  sbceq2g  3103  csbhypf  3120  csbiebt  3121  csbiebg  3124  dfss4st  3393  disjssun  3511  sneqrg  3789  preq12b  3797  preq12bg  3800  disji2  4023  iin0r  4199  opthg  4268  opeqsn  4282  unisucg  4446  opthreg  4589  tfisi  4620  dmsnopg  5138  relcoi1  5198  iotaeq  5224  iotabi  5225  fneq1  5343  fnun  5361  fnresdisj  5365  fnimadisj  5375  fnimaeq0  5376  sbcfng  5402  foeq1  5473  foco  5488  fveqeq2d  5563  fvelimab  5614  fvun1  5624  fvmptdv2  5648  fneqeql  5667  dffo3  5706  fvsng  5755  fconstfvm  5777  eufnfv  5790  f1veqaeq  5813  dff13f  5814  f1elima  5817  foeqcnvco  5834  f1eqcocnv  5835  acexmidlemab  5913  ovanraleqv  5943  eloprabga  6006  ovmpodv2  6053  ovi3  6057  ovelimab  6071  caovcang  6082  caovcan  6085  caovimo  6114  suppssfv  6128  suppssov1  6129  caofinvl  6157  uchoice  6192  op1stg  6205  op2ndg  6206  eqop  6232  reldm  6241  xporderlem  6286  tposfo2  6322  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  nnm0r  6534  nnmord  6572  nnaordex  6583  nnawordex  6584  ereq1  6596  eqerlem  6620  mapsn  6746  endisj  6880  pw2f1odclem  6892  xpf1o  6902  mapxpen  6906  fidifsnen  6928  supelti  7063  updjudhcoinlf  7141  updjudhcoinrg  7142  updjud  7143  omp1eomlem  7155  difinfsnlem  7160  nnnninfeq  7189  enomnilem  7199  finomni  7201  exmidomni  7203  fodjuomnilemres  7209  fodjuomni  7210  ismkvnex  7216  mkvprop  7219  fodjumkvlemres  7220  enmkvlem  7222  enwomnilem  7230  nninfdcinf  7232  nninfwlporlem  7234  nninfwlpoimlemginf  7237  pm54.43  7252  exmidfodomrlemrALT  7265  cc2lem  7328  addnidpig  7398  ltexpi  7399  dfplpq2  7416  dfmpq2  7417  recexnq  7452  recmulnqg  7453  ltexnqq  7470  halfnqq  7472  enq0tr  7496  nqnq0pi  7500  addnnnq0  7511  addlocpr  7598  ltexprlemru  7674  ltexpri  7675  lteupri  7679  prplnqu  7682  recexpr  7700  addsrpr  7807  mulsrpr  7808  00sr  7831  negexsr  7834  recexgt0sr  7835  srpospr  7845  prsrriota  7850  caucvgsrlemfv  7853  map2psrprg  7867  elrealeu  7891  axrnegex  7941  axprecex  7942  rereceu  7951  recriota  7952  nntopi  7956  axcaucvglemval  7959  axcaucvglemcau  7960  cnegexlem1  8196  cnegex  8199  cnegex2  8200  subval  8213  subadd  8224  subadd2  8225  subsub23  8226  addsubeq4  8236  subcan2  8246  negcon1  8273  subcan  8276  addrsub  8392  ltadd2  8440  ltordlem  8503  recexre  8599  recexap  8674  muleqadd  8689  receuap  8690  divvalap  8695  divmulap  8696  rec11ap  8731  rerecapb  8864  zdiv  9408  uzin  9628  xaddval  9914  xnn0xadd0  9936  xnegdi  9937  xltadd1  9945  icc0r  9995  fznlem  10110  fseq1m1p1  10164  1fv  10208  fzon  10236  fvinim0ffz  10311  ioo0  10331  ico0  10333  ioc0  10334  flqbi  10362  divfl0  10368  modq0  10403  modqmuladdnn0  10442  addmodlteq  10472  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  seq3f1olemstep  10588  seq3f1olemp  10589  seq3id  10599  seq3z  10602  qsqeqor  10724  mulreap  11011  rennim  11149  resqrexlemex  11172  rsqrmo  11174  resqrtcl  11176  rersqrtthlem  11177  sqrtsq2  11190  isumss  11537  fsum00  11608  telfsumo  11612  pwm1geoserap1  11654  prodssdc  11735  absefib  11917  efieq1re  11918  divides  11935  dvdsval2  11936  nndivides  11943  dvds0lem  11947  dvds1lem  11948  dvds2lem  11949  negdvdsb  11953  muldvds1  11962  muldvds2  11963  dvdscmulr  11966  dvdsmulcr  11967  dvdstr  11974  dvdsabseq  11992  divconjdvds  11994  odd2np1lem  12016  odd2np1  12017  even2n  12018  oddm1even  12019  2tp1odd  12028  opeo  12041  omeo  12042  m1exp1  12045  divalgb  12069  gcdaddm  12124  gcdabs1  12129  bezout  12151  gcdmultiple  12160  gcdmultiplez  12161  rplpwr  12167  rppwr  12168  nninfctlemfo  12180  alginv  12188  algcvga  12192  algfx  12193  eucalgval2  12194  coprmdvds  12233  qredeq  12237  qredeu  12238  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  rpexp  12294  rpexp12i  12296  cncongrprm  12298  qnumdenbi  12333  phival  12354  phicl2  12355  dfphi2  12361  phiprmpw  12363  phimullem  12366  eulerthlem1  12368  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlemth  12373  eulerth  12374  fermltl  12375  hashgcdlem  12379  phisum  12381  odzval  12382  odzdvds  12386  reumodprminv  12394  modprm0  12395  nnnn0modprm0  12396  modprmn0modprm0  12397  coprimeprodsq  12398  coprimeprodsq2  12399  pythagtriplem2  12407  pythagtrip  12424  pceulem  12435  pcval  12437  pcqmul  12444  pcqcl  12447  pcabs  12467  pc2dvds  12471  pcaddlem  12480  pcadd  12481  pcmpt  12484  prmpwdvds  12496  pockthi  12499  4sqlem12  12543  ennnfonelemhf1o  12573  fvprif  12929  mgmidmo  12958  grpidvalg  12959  grpidpropdg  12960  ismgmid  12963  ismgmid2  12966  mgmidsssn0  12970  grpinvalem  12971  grprida  12973  igsumvalx  12975  gsumress  12981  ismnddef  13002  sgrpidmndm  13004  ismndd  13021  mndpropd  13024  mndinvmod  13029  mnd1  13030  ismhm  13036  gsumvallem2  13068  grpinvex  13085  isgrpd2  13096  isgrpd  13098  dfgrp2  13102  grpinveu  13113  grpinvval  13118  grplinv  13125  isgrpinv  13129  grplrinv  13132  grpidinv2  13133  grpidinv  13134  grplmulf1o  13149  grpsubeq0  13161  grpsubadd  13163  dfgrp3mlem  13173  dfgrp3m  13174  grp1  13181  imasgrp2  13183  qusgrp2  13186  mhmmnd  13189  ghmgrp  13191  mulgval  13195  mulgaddcom  13219  eqg0el  13302  ghmeqker  13344  ghmf1  13346  conjnmzb  13353  ablsubadd  13385  ablsubsub23  13398  rngmneg1  13446  rngmneg2  13447  dfur2g  13461  srgideu  13471  srgidmlem  13477  issrgid  13480  srgrz  13483  srglz  13484  srgisid  13485  srg1zr  13486  ringideu  13516  ringidmlem  13521  isringid  13524  ringid  13525  qusring2  13565  oppr0g  13580  oppr1g  13581  reldvdsrsrg  13591  dvdsrvald  13592  dvdsrmuld  13595  dvdsr01  13603  dvdsr02  13604  opprunitd  13609  crngunit  13610  unitinvinv  13623  dvreq1  13641  dvdsrpropdg  13646  rhmdvdsr  13674  lringuplu  13695  subrg1  13730  subrgdvds  13734  isrrg  13762  rrgeq0i  13763  rrgeq0  13764  domneq0  13771  islmod  13790  islmodd  13792  lmodprop2d  13847  lss1d  13882  cnfldui  14088  znval  14135  znidom  14156  znunit  14158  znrrg  14159  ntreq0  14311  ispsmet  14502  psmet0  14506  ismet  14523  isxmet  14524  xmeteq0  14538  metn0  14557  xmetres2  14558  xblss2ps  14583  xblss2  14584  xmseq0  14647  comet  14678  bdxmet  14680  cnmet  14709  ivthdec  14823  ivthreinc  14824  elply2  14914  reeff1o  14949  ioocosf1o  15030  logbgcd1irr  15140  logbgcd1irraplemexp  15141  lgsval  15161  lgsdir  15192  lgsne0  15195  lgsprme0  15199  lgsdirnn0  15204  gausslemma2dlem0c  15208  gausslemma2dlem0i  15214  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem2  15228  lgseisenlem3  15229  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  lgsquad3  15241  m1lgs  15242  2lgs  15261  2sqlem7  15278  2sqlem8  15280  2sqlem9  15281  bj-charfunbi  15373  pwle2  15559  subctctexmid  15561  peano4nninf  15566  nninfalllem1  15568  nninfsellemdc  15570  nninfsellemeq  15574  nninfsellemqall  15575  nninfsellemeqinf  15576  isomninnlem  15590  trilpolemlt1  15601  trirec0  15604  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  dceqnconst  15620  dcapnconst  15621