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  4308  opthg  4380  opeqsn  4395  unisucg  4561  opthreg  4705  tfisi  4736  dmsnopg  5262  relcoi1  5322  iotaeq  5349  iotabi  5350  fneq1  5472  fnun  5492  fnresdisj  5496  fnimadisj  5507  fnimaeq0  5508  sbcfng  5534  foeq1  5614  foco  5629  fveqeq2d  5706  fvelimab  5762  fvun1  5772  fvmptdv2  5798  fneqeql  5820  dffo3  5858  fvsng  5914  fconstfvm  5936  eufnfv  5952  f1veqaeq  5978  dff13f  5979  f1elima  5982  foeqcnvco  5999  f1eqcocnv  6000  acexmidlemab  6082  ovanraleqv  6112  eloprabga  6178  ovmpodv2  6225  ovi3  6229  ovelimab  6243  caovcang  6254  caovcan  6257  caovimo  6286  suppssov1  6302  caofinvl  6332  caofid1  6335  caofid2  6336  uchoice  6375  op1stg  6388  op2ndg  6389  eqop  6415  reldm  6424  xporderlem  6471  suppofss1dcl  6508  suppofss2dcl  6509  tposfo2  6542  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  nnm0r  6756  nnmord  6794  nnaordex  6805  nnawordex  6806  ereq1  6818  eqerlem  6842  mapsnd  6974  mapsn  6976  endisj  7126  pw2f1odclem  7138  xpf1o  7148  mapxpen  7152  fidifsnen  7176  2omap  7324  supelti  7348  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  omp1eomlem  7440  difinfsnlem  7445  nnnninfeq  7474  enomnilem  7484  finomni  7486  exmidomni  7488  fodjuomnilemres  7494  fodjuomni  7495  ismkvnex  7501  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemginf  7522  pm54.43  7542  exmidfodomrlemrALT  7561  cc2lem  7638  addnidpig  7709  ltexpi  7710  dfplpq2  7727  dfmpq2  7728  recexnq  7763  recmulnqg  7764  ltexnqq  7781  halfnqq  7783  enq0tr  7807  nqnq0pi  7811  addnnnq0  7822  addlocpr  7909  ltexprlemru  7985  ltexpri  7986  lteupri  7990  prplnqu  7993  recexpr  8011  addsrpr  8118  mulsrpr  8119  00sr  8142  negexsr  8145  recexgt0sr  8146  srpospr  8156  prsrriota  8161  caucvgsrlemfv  8164  map2psrprg  8178  elrealeu  8202  axrnegex  8252  axprecex  8253  rereceu  8262  recriota  8263  nntopi  8267  axcaucvglemval  8270  axcaucvglemcau  8271  cnegexlem1  8508  cnegex  8511  cnegex2  8512  subval  8525  subadd  8536  subadd2  8537  subsub23  8538  addsubeq4  8548  subcan2  8558  negcon1  8585  subcan  8588  addrsub  8704  ltadd2  8754  ltordlem  8817  recexre  8914  recexap  8989  muleqadd  9006  receuap  9007  divvalap  9012  divmulap  9013  rec11ap  9048  rerecapb  9181  zdiv  9745  uzin  9971  xaddval  10264  xnn0xadd0  10286  xnegdi  10287  xltadd1  10295  icc0r  10345  fznlem  10462  fseq1m1p1  10519  1fv  10563  fzon  10591  fvinim0ffz  10677  ioo0  10711  ico0  10713  ioc0  10714  flqbi  10746  divfl0  10752  modq0  10787  modqmuladdnn0  10826  addmodlteq  10856  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seq3f1olemstep  10972  seq3f1olemp  10973  seq3id  10983  seq3z  10986  qsqeqor  11108  hashfibc  11305  hashf1lem1  11307  hashtpglem  11320  ccat0  11386  wrdl1s1  11420  ccatws1lenp1bg  11425  pfxsuff1eqwrdeq  11493  swrdccatin2  11523  pfxccatin12lem2  11525  mulreap  11651  rennim  11790  resqrexlemex  11813  rsqrmo  11815  resqrtcl  11817  rersqrtthlem  11818  sqrtsq2  11831  isumss  12183  fsum00  12254  telfsumo  12258  pwm1geoserap1  12300  prodssdc  12381  absefib  12563  efieq1re  12564  divides  12581  dvdsval2  12582  nndivides  12589  dvds0lem  12593  dvds1lem  12594  dvds2lem  12595  negdvdsb  12599  muldvds1  12608  muldvds2  12609  dvdscmulr  12612  dvdsmulcr  12613  dvdstr  12620  dvdsabseq  12639  divconjdvds  12641  odd2np1lem  12664  odd2np1  12665  even2n  12666  oddm1even  12667  2tp1odd  12676  opeo  12689  omeo  12690  m1exp1  12693  divalgb  12717  gcdaddm  12786  gcdabs1  12791  bezout  12813  gcdmultiple  12822  gcdmultiplez  12823  rplpwr  12829  rppwr  12830  nninfctlemfo  12842  alginv  12850  algcvga  12854  algfx  12855  eucalgval2  12856  coprmdvds  12895  qredeq  12899  qredeu  12900  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  rpexp  12957  rpexp12i  12959  cncongrprm  12961  qnumdenbi  12997  phival  13020  phicl2  13021  dfphi2  13027  phiprmpw  13029  phimullem  13032  eulerthlem1  13034  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlemth  13039  eulerth  13040  fermltl  13041  hashgcdlem  13045  phisum  13048  odzval  13049  odzdvds  13053  reumodprminv  13061  modprm0  13062  nnnn0modprm0  13063  modprmn0modprm0  13064  coprimeprodsq  13065  coprimeprodsq2  13066  pythagtriplem2  13074  pythagtrip  13091  pceulem  13102  pcval  13104  pcqmul  13111  pcqcl  13114  pcabs  13134  pc2dvds  13138  pcaddlem  13147  pcadd  13148  pcmpt  13151  prmpwdvds  13163  pockthi  13166  4sqlem12  13210  ballotfilemi  13301  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemsima  13317  ballotfilemfrcn0  13331  ballotfi  13340  ennnfonelemhf1o  13362  fvprif  13723  mgmidmo  13751  grpidvalg  13752  grpidpropdg  13753  ismgmid  13756  ismgmid2  13759  mgmidsssn0  13763  grpinvalem  13764  grprida  13766  gzsumvalx  13768  gzsumress  13771  ismnddef  13790  sgrpidmndm  13792  ismndd  13809  mndpropd  13812  mndinvmod  13817  mnd1  13821  ismhm  13827  gsumvallem2  13859  grpinvex  13874  isgrpd2  13885  isgrpd  13887  dfgrp2  13891  grpinveu  13902  grpinvval  13907  grplinv  13914  isgrpinv  13918  grplrinv  13921  grpidinv2  13922  grpidinv  13923  grplmulf1o  13938  grpsubeq0  13950  grpsubadd  13952  dfgrp3mlem  13962  dfgrp3m  13963  grp1  13970  imasgrp2  13972  qusgrp2  13975  mhmmnd  13978  ghmgrp  13980  mulgval  13984  mulgaddcom  14008  eqg0el  14091  ghmeqker  14133  ghmf1  14135  conjnmzb  14142  ablsubadd  14206  ablsubsub23  14219  gsumzfi  14248  gsumsnfdcmn  14257  rngmneg1  14353  rngmneg2  14354  rng1zrlem  14365  dfur2g  14373  srgideu  14383  srgidmlem  14389  issrgid  14392  srgrz  14395  srglz  14396  srgisid  14397  ringideu  14428  ringidmlem  14434  isringid  14437  ringid  14438  qusring2  14480  oppr0g  14496  oppr1g  14497  dvdsrvald  14509  dvdsrmuld  14512  dvdsr01  14520  dvdsr02  14521  opprunitd  14526  crngunit  14527  unitinvinv  14540  dvreq1  14558  dvdsrpropdg  14563  rhmdvdsr  14591  lringuplu  14612  subrg1  14648  subrgdvds  14652  isrrg  14680  rrgeq0i  14681  rrgeq0  14682  domneq0  14690  islmod  14736  islmodd  14738  lmodprop2d  14794  lss1d  14829  cnfldui  15033  znval  15080  znidom  15101  znunit  15103  znrrg  15104  psrlidmfi  15199  psrridmfi  15200  mplelbascoe  15208  ntreq0  15358  ispsmet  15549  psmet0  15553  ismet  15570  isxmet  15571  xmeteq0  15585  metn0  15604  xmetres2  15605  xblss2ps  15630  xblss2  15631  xmseq0  15694  comet  15725  bdxmet  15727  cnmet  15756  ivthdec  15870  ivthreinc  15871  elply2  15961  reeff1o  15999  sineq0re  16076  ioocosf1o  16082  efnthr  16176  logbgcd1irr  16203  logbgcd1irraplemexp  16204  birthdaylem1g  16225  mpodvdsmulf1o  16284  ppiqub  16293  lgsval  16328  lgsdir  16359  lgsne0  16362  lgsprme0  16366  lgsdirnn0  16371  gausslemma2dlem0c  16375  gausslemma2dlem0i  16381  gausslemma2dlem7  16392  gausslemma2d  16393  lgseisenlem2  16395  lgseisenlem3  16396  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  lgsquad3  16408  m1lgs  16409  2lgs  16428  2sqlem7  16445  2sqlem8  16447  2sqlem9  16448  edg0iedg0g  16512  upgredg  16590  ushgredgedgloop  16674  edg0usgr  16693  vtxdgfval  16734  vtxdgop  16738  vtxdeqd  16742  vtxdfifiun  16743  vtxd0nedgbfi  16745  1loopgrvd2fi  16751  wksfval  16768  wlklenvclwlk  16819  clwwlknon  16875  isclwwlknon  16876  s2elclwwlknon2  16882  depind  16955  dichmul0orlem7  16964  bj-charfunbi  17042  pw1map  17230  pwle2  17233  subctctexmid  17235  wexmiddifxylem  17250  peano4nninf  17255  nninfalllem1  17257  nninfsellemdc  17259  nninfsellemeq  17263  nninfsellemqall  17264  nninfsellemeqinf  17265  isomninnlem  17285  trilpolemlt1  17297  trirec0  17300  qdiff  17305  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  dceqnconst  17317  dcapnconst  17318