Theorem eqeq1d 2238

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 2236	. 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 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  rspcedeq1vd  2916  sbceq2g  3146  csbhypf  3163  csbiebt  3164  csbiebg  3167  dfss4st  3437  disjssun  3555  sneqrg  3840  preq12b  3848  preq12bg  3851  disji2  4075  invdisjrab  4077  iin0r  4253  opthg  4324  opeqsn  4339  unisucg  4505  opthreg  4648  tfisi  4679  dmsnopg  5200  relcoi1  5260  iotaeq  5287  iotabi  5288  fneq1  5409  fnun  5429  fnresdisj  5433  fnimadisj  5444  fnimaeq0  5445  sbcfng  5471  foeq1  5546  foco  5561  fveqeq2d  5637  fvelimab  5692  fvun1  5702  fvmptdv2  5726  fneqeql  5745  dffo3  5784  fvsng  5839  fconstfvm  5861  eufnfv  5874  f1veqaeq  5899  dff13f  5900  f1elima  5903  foeqcnvco  5920  f1eqcocnv  5921  acexmidlemab  6001  ovanraleqv  6031  eloprabga  6097  ovmpodv2  6144  ovi3  6148  ovelimab  6162  caovcang  6173  caovcan  6176  caovimo  6205  suppssfv  6220  suppssov1  6221  caofinvl  6250  caofid1  6253  caofid2  6254  uchoice  6289  op1stg  6302  op2ndg  6303  eqop  6329  reldm  6338  xporderlem  6383  tposfo2  6419  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnm0r  6633  nnmord  6671  nnaordex  6682  nnawordex  6683  ereq1  6695  eqerlem  6719  mapsn  6845  endisj  6991  pw2f1odclem  7003  xpf1o  7013  mapxpen  7017  fidifsnen  7040  supelti  7180  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  omp1eomlem  7272  difinfsnlem  7277  nnnninfeq  7306  enomnilem  7316  finomni  7318  exmidomni  7320  fodjuomnilemres  7326  fodjuomni  7327  ismkvnex  7333  mkvprop  7336  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemginf  7354  pm54.43  7374  exmidfodomrlemrALT  7392  cc2lem  7463  addnidpig  7534  ltexpi  7535  dfplpq2  7552  dfmpq2  7553  recexnq  7588  recmulnqg  7589  ltexnqq  7606  halfnqq  7608  enq0tr  7632  nqnq0pi  7636  addnnnq0  7647  addlocpr  7734  ltexprlemru  7810  ltexpri  7811  lteupri  7815  prplnqu  7818  recexpr  7836  addsrpr  7943  mulsrpr  7944  00sr  7967  negexsr  7970  recexgt0sr  7971  srpospr  7981  prsrriota  7986  caucvgsrlemfv  7989  map2psrprg  8003  elrealeu  8027  axrnegex  8077  axprecex  8078  rereceu  8087  recriota  8088  nntopi  8092  axcaucvglemval  8095  axcaucvglemcau  8096  cnegexlem1  8332  cnegex  8335  cnegex2  8336  subval  8349  subadd  8360  subadd2  8361  subsub23  8362  addsubeq4  8372  subcan2  8382  negcon1  8409  subcan  8412  addrsub  8528  ltadd2  8577  ltordlem  8640  recexre  8736  recexap  8811  muleqadd  8826  receuap  8827  divvalap  8832  divmulap  8833  rec11ap  8868  rerecapb  9001  zdiv  9546  uzin  9767  xaddval  10053  xnn0xadd0  10075  xnegdi  10076  xltadd1  10084  icc0r  10134  fznlem  10249  fseq1m1p1  10303  1fv  10347  fzon  10375  fvinim0ffz  10459  ioo0  10491  ico0  10493  ioc0  10494  flqbi  10522  divfl0  10528  modq0  10563  modqmuladdnn0  10602  addmodlteq  10632  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seq3f1olemstep  10748  seq3f1olemp  10749  seq3id  10759  seq3z  10762  qsqeqor  10884  ccat0  11144  wrdl1s1  11178  ccatws1lenp1bg  11183  pfxsuff1eqwrdeq  11247  swrdccatin2  11277  pfxccatin12lem2  11279  mulreap  11391  rennim  11529  resqrexlemex  11552  rsqrmo  11554  resqrtcl  11556  rersqrtthlem  11557  sqrtsq2  11570  isumss  11918  fsum00  11989  telfsumo  11993  pwm1geoserap1  12035  prodssdc  12116  absefib  12298  efieq1re  12299  divides  12316  dvdsval2  12317  nndivides  12324  dvds0lem  12328  dvds1lem  12329  dvds2lem  12330  negdvdsb  12334  muldvds1  12343  muldvds2  12344  dvdscmulr  12347  dvdsmulcr  12348  dvdstr  12355  dvdsabseq  12374  divconjdvds  12376  odd2np1lem  12399  odd2np1  12400  even2n  12401  oddm1even  12402  2tp1odd  12411  opeo  12424  omeo  12425  m1exp1  12428  divalgb  12452  gcdaddm  12521  gcdabs1  12526  bezout  12548  gcdmultiple  12557  gcdmultiplez  12558  rplpwr  12564  rppwr  12565  nninfctlemfo  12577  alginv  12585  algcvga  12589  algfx  12590  eucalgval2  12591  coprmdvds  12630  qredeq  12634  qredeu  12635  divgcdcoprm0  12639  divgcdcoprmex  12640  cncongr1  12641  rpexp  12691  rpexp12i  12693  cncongrprm  12695  qnumdenbi  12730  phival  12751  phicl2  12752  dfphi2  12758  phiprmpw  12760  phimullem  12763  eulerthlem1  12765  eulerthlemfi  12766  eulerthlemrprm  12767  eulerthlemth  12770  eulerth  12771  fermltl  12772  hashgcdlem  12776  phisum  12779  odzval  12780  odzdvds  12784  reumodprminv  12792  modprm0  12793  nnnn0modprm0  12794  modprmn0modprm0  12795  coprimeprodsq  12796  coprimeprodsq2  12797  pythagtriplem2  12805  pythagtrip  12822  pceulem  12833  pcval  12835  pcqmul  12842  pcqcl  12845  pcabs  12865  pc2dvds  12869  pcaddlem  12878  pcadd  12879  pcmpt  12882  prmpwdvds  12894  pockthi  12897  4sqlem12  12941  ennnfonelemhf1o  13000  fvprif  13392  mgmidmo  13421  grpidvalg  13422  grpidpropdg  13423  ismgmid  13426  ismgmid2  13429  mgmidsssn0  13433  grpinvalem  13434  grprida  13436  igsumvalx  13438  gsumress  13444  ismnddef  13467  sgrpidmndm  13469  ismndd  13486  mndpropd  13489  mndinvmod  13494  mnd1  13504  ismhm  13510  gsumvallem2  13542  grpinvex  13559  isgrpd2  13570  isgrpd  13572  dfgrp2  13576  grpinveu  13587  grpinvval  13592  grplinv  13599  isgrpinv  13603  grplrinv  13606  grpidinv2  13607  grpidinv  13608  grplmulf1o  13623  grpsubeq0  13635  grpsubadd  13637  dfgrp3mlem  13647  dfgrp3m  13648  grp1  13655  imasgrp2  13663  qusgrp2  13666  mhmmnd  13669  ghmgrp  13671  mulgval  13675  mulgaddcom  13699  eqg0el  13782  ghmeqker  13824  ghmf1  13826  conjnmzb  13833  ablsubadd  13865  ablsubsub23  13878  rngmneg1  13926  rngmneg2  13927  dfur2g  13941  srgideu  13951  srgidmlem  13957  issrgid  13960  srgrz  13963  srglz  13964  srgisid  13965  srg1zr  13966  ringideu  13996  ringidmlem  14001  isringid  14004  ringid  14005  qusring2  14045  oppr0g  14060  oppr1g  14061  dvdsrvald  14073  dvdsrmuld  14076  dvdsr01  14084  dvdsr02  14085  opprunitd  14090  crngunit  14091  unitinvinv  14104  dvreq1  14122  dvdsrpropdg  14127  rhmdvdsr  14155  lringuplu  14176  subrg1  14211  subrgdvds  14215  isrrg  14243  rrgeq0i  14244  rrgeq0  14245  domneq0  14252  islmod  14271  islmodd  14273  lmodprop2d  14328  lss1d  14363  cnfldui  14569  znval  14616  znidom  14637  znunit  14639  znrrg  14640  mplelbascoe  14672  ntreq0  14822  ispsmet  15013  psmet0  15017  ismet  15034  isxmet  15035  xmeteq0  15049  metn0  15068  xmetres2  15069  xblss2ps  15094  xblss2  15095  xmseq0  15158  comet  15189  bdxmet  15191  cnmet  15220  ivthdec  15334  ivthreinc  15335  elply2  15425  reeff1o  15463  ioocosf1o  15544  logbgcd1irr  15657  logbgcd1irraplemexp  15658  mpodvdsmulf1o  15680  lgsval  15699  lgsdir  15730  lgsne0  15733  lgsprme0  15737  lgsdirnn0  15742  gausslemma2dlem0c  15746  gausslemma2dlem0i  15752  gausslemma2dlem7  15763  gausslemma2d  15764  lgseisenlem2  15766  lgseisenlem3  15767  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem2  15777  lgsquad3  15779  m1lgs  15780  2lgs  15799  2sqlem7  15816  2sqlem8  15818  2sqlem9  15819  edg0iedg0g  15882  upgredg  15958  ushgredgedgloop  16042  vtxdgfval  16048  vtxdgop  16052  vtxdeqd  16056  vtxdfifiun  16057  vtxd0nedgbfi  16059  wksfval  16068  wlklenvclwlk  16119  bj-charfunbi  16257  2omap  16446  pw1map  16448  pwle2  16451  subctctexmid  16453  peano4nninf  16460  nninfalllem1  16462  nninfsellemdc  16464  nninfsellemeq  16468  nninfsellemqall  16469  nninfsellemeqinf  16470  isomninnlem  16486  trilpolemlt1  16497  trirec0  16500  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508  dceqnconst  16516  dcapnconst  16517