Theorem eqeq1d 2247

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 2245	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A = C <-> B = C ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  rspcedeq1vd  2939  sbceq2g  3169  csbhypf  3186  csbiebt  3187  csbiebg  3190  dfss4st  3464  disjssun  3588  sneqrg  3887  preq12b  3895  preq12bg  3898  disji2  4122  invdisjrab  4124  iin0r  4306  opthg  4378  opeqsn  4393  unisucg  4559  opthreg  4703  tfisi  4734  dmsnopg  5259  relcoi1  5319  iotaeq  5346  iotabi  5347  fneq1  5469  fnun  5489  fnresdisj  5493  fnimadisj  5504  fnimaeq0  5505  sbcfng  5531  foeq1  5611  foco  5626  fveqeq2d  5703  fvelimab  5759  fvun1  5769  fvmptdv2  5795  fneqeql  5817  dffo3  5855  fvsng  5911  fconstfvm  5933  eufnfv  5949  f1veqaeq  5975  dff13f  5976  f1elima  5979  foeqcnvco  5996  f1eqcocnv  5997  acexmidlemab  6079  ovanraleqv  6109  eloprabga  6175  ovmpodv2  6222  ovi3  6226  ovelimab  6240  caovcang  6251  caovcan  6254  caovimo  6283  suppssov1  6299  caofinvl  6328  caofid1  6331  caofid2  6332  uchoice  6371  op1stg  6384  op2ndg  6385  eqop  6411  reldm  6420  xporderlem  6467  suppofss1dcl  6504  suppofss2dcl  6505  tposfo2  6538  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnm0r  6752  nnmord  6790  nnaordex  6801  nnawordex  6802  ereq1  6814  eqerlem  6838  mapsnd  6970  mapsn  6972  endisj  7122  pw2f1odclem  7134  xpf1o  7144  mapxpen  7148  fidifsnen  7172  2omap  7319  supelti  7343  updjudhcoinlf  7421  updjudhcoinrg  7422  updjud  7423  omp1eomlem  7435  difinfsnlem  7440  nnnninfeq  7469  enomnilem  7479  finomni  7481  exmidomni  7483  fodjuomnilemres  7489  fodjuomni  7490  ismkvnex  7496  mkvprop  7499  fodjumkvlemres  7500  enmkvlem  7502  enwomnilem  7510  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemginf  7517  pm54.43  7537  exmidfodomrlemrALT  7556  cc2lem  7633  addnidpig  7704  ltexpi  7705  dfplpq2  7722  dfmpq2  7723  recexnq  7758  recmulnqg  7759  ltexnqq  7776  halfnqq  7778  enq0tr  7802  nqnq0pi  7806  addnnnq0  7817  addlocpr  7904  ltexprlemru  7980  ltexpri  7981  lteupri  7985  prplnqu  7988  recexpr  8006  addsrpr  8113  mulsrpr  8114  00sr  8137  negexsr  8140  recexgt0sr  8141  srpospr  8151  prsrriota  8156  caucvgsrlemfv  8159  map2psrprg  8173  elrealeu  8197  axrnegex  8247  axprecex  8248  rereceu  8257  recriota  8258  nntopi  8262  axcaucvglemval  8265  axcaucvglemcau  8266  cnegexlem1  8503  cnegex  8506  cnegex2  8507  subval  8520  subadd  8531  subadd2  8532  subsub23  8533  addsubeq4  8543  subcan2  8553  negcon1  8580  subcan  8583  addrsub  8699  ltadd2  8749  ltordlem  8812  recexre  8909  recexap  8984  muleqadd  9001  receuap  9002  divvalap  9007  divmulap  9008  rec11ap  9043  rerecapb  9176  zdiv  9739  uzin  9965  xaddval  10258  xnn0xadd0  10280  xnegdi  10281  xltadd1  10289  icc0r  10339  fznlem  10456  fseq1m1p1  10513  1fv  10557  fzon  10585  fvinim0ffz  10671  ioo0  10705  ico0  10707  ioc0  10708  flqbi  10740  divfl0  10746  modq0  10781  modqmuladdnn0  10820  addmodlteq  10850  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  seq3f1olemstep  10966  seq3f1olemp  10967  seq3id  10977  seq3z  10980  qsqeqor  11102  hashfibc  11299  hashf1lem1  11301  hashtpglem  11314  ccat0  11380  wrdl1s1  11414  ccatws1lenp1bg  11419  pfxsuff1eqwrdeq  11487  swrdccatin2  11517  pfxccatin12lem2  11519  mulreap  11645  rennim  11784  resqrexlemex  11807  rsqrmo  11809  resqrtcl  11811  rersqrtthlem  11812  sqrtsq2  11825  isumss  12177  fsum00  12248  telfsumo  12252  pwm1geoserap1  12294  prodssdc  12375  absefib  12557  efieq1re  12558  divides  12575  dvdsval2  12576  nndivides  12583  dvds0lem  12587  dvds1lem  12588  dvds2lem  12589  negdvdsb  12593  muldvds1  12602  muldvds2  12603  dvdscmulr  12606  dvdsmulcr  12607  dvdstr  12614  dvdsabseq  12633  divconjdvds  12635  odd2np1lem  12658  odd2np1  12659  even2n  12660  oddm1even  12661  2tp1odd  12670  opeo  12683  omeo  12684  m1exp1  12687  divalgb  12711  gcdaddm  12780  gcdabs1  12785  bezout  12807  gcdmultiple  12816  gcdmultiplez  12817  rplpwr  12823  rppwr  12824  nninfctlemfo  12836  alginv  12844  algcvga  12848  algfx  12849  eucalgval2  12850  coprmdvds  12889  qredeq  12893  qredeu  12894  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  rpexp  12951  rpexp12i  12953  cncongrprm  12955  qnumdenbi  12991  phival  13014  phicl2  13015  dfphi2  13021  phiprmpw  13023  phimullem  13026  eulerthlem1  13028  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlemth  13033  eulerth  13034  fermltl  13035  hashgcdlem  13039  phisum  13042  odzval  13043  odzdvds  13047  reumodprminv  13055  modprm0  13056  nnnn0modprm0  13057  modprmn0modprm0  13058  coprimeprodsq  13059  coprimeprodsq2  13060  pythagtriplem2  13068  pythagtrip  13085  pceulem  13096  pcval  13098  pcqmul  13105  pcqcl  13108  pcabs  13128  pc2dvds  13132  pcaddlem  13141  pcadd  13142  pcmpt  13145  prmpwdvds  13157  pockthi  13160  4sqlem12  13204  ballotfilemi  13295  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemsima  13311  ballotfilemfrcn0  13325  ballotfi  13334  ennnfonelemhf1o  13356  fvprif  13717  mgmidmo  13745  grpidvalg  13746  grpidpropdg  13747  ismgmid  13750  ismgmid2  13753  mgmidsssn0  13757  grpinvalem  13758  grprida  13760  gzsumvalx  13762  gzsumress  13765  ismnddef  13784  sgrpidmndm  13786  ismndd  13803  mndpropd  13806  mndinvmod  13811  mnd1  13815  ismhm  13821  gsumvallem2  13853  grpinvex  13868  isgrpd2  13879  isgrpd  13881  dfgrp2  13885  grpinveu  13896  grpinvval  13901  grplinv  13908  isgrpinv  13912  grplrinv  13915  grpidinv2  13916  grpidinv  13917  grplmulf1o  13932  grpsubeq0  13944  grpsubadd  13946  dfgrp3mlem  13956  dfgrp3m  13957  grp1  13964  imasgrp2  13966  qusgrp2  13969  mhmmnd  13972  ghmgrp  13974  mulgval  13978  mulgaddcom  14002  eqg0el  14085  ghmeqker  14127  ghmf1  14129  conjnmzb  14136  ablsubadd  14200  ablsubsub23  14213  gsumzfi  14242  rngmneg1  14330  rngmneg2  14331  rng1zrlem  14342  dfur2g  14350  srgideu  14360  srgidmlem  14366  issrgid  14369  srgrz  14372  srglz  14373  srgisid  14374  ringideu  14405  ringidmlem  14411  isringid  14414  ringid  14415  qusring2  14455  oppr0g  14471  oppr1g  14472  dvdsrvald  14484  dvdsrmuld  14487  dvdsr01  14495  dvdsr02  14496  opprunitd  14501  crngunit  14502  unitinvinv  14515  dvreq1  14533  dvdsrpropdg  14538  rhmdvdsr  14566  lringuplu  14587  subrg1  14623  subrgdvds  14627  isrrg  14655  rrgeq0i  14656  rrgeq0  14657  domneq0  14665  islmod  14711  islmodd  14713  lmodprop2d  14769  lss1d  14804  cnfldui  15008  znval  15055  znidom  15076  znunit  15078  znrrg  15079  mplelbascoe  15174  ntreq0  15324  ispsmet  15515  psmet0  15519  ismet  15536  isxmet  15537  xmeteq0  15551  metn0  15570  xmetres2  15571  xblss2ps  15596  xblss2  15597  xmseq0  15660  comet  15691  bdxmet  15693  cnmet  15722  ivthdec  15836  ivthreinc  15837  elply2  15927  reeff1o  15965  ioocosf1o  16047  logbgcd1irr  16164  logbgcd1irraplemexp  16165  birthdaylem1g  16186  mpodvdsmulf1o  16245  ppiqub  16254  lgsval  16289  lgsdir  16320  lgsne0  16323  lgsprme0  16327  lgsdirnn0  16332  gausslemma2dlem0c  16336  gausslemma2dlem0i  16342  gausslemma2dlem7  16353  gausslemma2d  16354  lgseisenlem2  16356  lgseisenlem3  16357  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  lgsquad3  16369  m1lgs  16370  2lgs  16389  2sqlem7  16406  2sqlem8  16408  2sqlem9  16409  edg0iedg0g  16473  upgredg  16551  ushgredgedgloop  16635  edg0usgr  16654  vtxdgfval  16695  vtxdgop  16699  vtxdeqd  16703  vtxdfifiun  16704  vtxd0nedgbfi  16706  1loopgrvd2fi  16712  wksfval  16729  wlklenvclwlk  16780  clwwlknon  16836  isclwwlknon  16837  s2elclwwlknon2  16843  depind  16916  dichmul0orlem7  16925  bj-charfunbi  17003  pw1map  17191  pwle2  17194  subctctexmid  17196  wexmiddifxylem  17211  peano4nninf  17215  nninfalllem1  17217  nninfsellemdc  17219  nninfsellemeq  17223  nninfsellemqall  17224  nninfsellemeqinf  17225  isomninnlem  17245  trilpolemlt1  17257  trirec0  17260  qdiff  17265  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  dceqnconst  17277  dcapnconst  17278