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  4254  opthg  4325  opeqsn  4340  unisucg  4506  opthreg  4649  tfisi  4680  dmsnopg  5203  relcoi1  5263  iotaeq  5290  iotabi  5291  fneq1  5412  fnun  5432  fnresdisj  5436  fnimadisj  5447  fnimaeq0  5448  sbcfng  5474  foeq1  5549  foco  5564  fveqeq2d  5640  fvelimab  5695  fvun1  5705  fvmptdv2  5729  fneqeql  5748  dffo3  5787  fvsng  5842  fconstfvm  5864  eufnfv  5877  f1veqaeq  5902  dff13f  5903  f1elima  5906  foeqcnvco  5923  f1eqcocnv  5924  acexmidlemab  6004  ovanraleqv  6034  eloprabga  6100  ovmpodv2  6147  ovi3  6151  ovelimab  6165  caovcang  6176  caovcan  6179  caovimo  6208  suppssfv  6223  suppssov1  6224  caofinvl  6253  caofid1  6256  caofid2  6257  uchoice  6292  op1stg  6305  op2ndg  6306  eqop  6332  reldm  6341  xporderlem  6388  tposfo2  6424  frec0g  6554  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecsuc  6564  nnm0r  6638  nnmord  6676  nnaordex  6687  nnawordex  6688  ereq1  6700  eqerlem  6724  mapsn  6850  endisj  6996  pw2f1odclem  7008  xpf1o  7018  mapxpen  7022  fidifsnen  7045  supelti  7185  updjudhcoinlf  7263  updjudhcoinrg  7264  updjud  7265  omp1eomlem  7277  difinfsnlem  7282  nnnninfeq  7311  enomnilem  7321  finomni  7323  exmidomni  7325  fodjuomnilemres  7331  fodjuomni  7332  ismkvnex  7338  mkvprop  7341  fodjumkvlemres  7342  enmkvlem  7344  enwomnilem  7352  nninfdcinf  7354  nninfwlporlem  7356  nninfwlpoimlemginf  7359  pm54.43  7379  exmidfodomrlemrALT  7397  cc2lem  7468  addnidpig  7539  ltexpi  7540  dfplpq2  7557  dfmpq2  7558  recexnq  7593  recmulnqg  7594  ltexnqq  7611  halfnqq  7613  enq0tr  7637  nqnq0pi  7641  addnnnq0  7652  addlocpr  7739  ltexprlemru  7815  ltexpri  7816  lteupri  7820  prplnqu  7823  recexpr  7841  addsrpr  7948  mulsrpr  7949  00sr  7972  negexsr  7975  recexgt0sr  7976  srpospr  7986  prsrriota  7991  caucvgsrlemfv  7994  map2psrprg  8008  elrealeu  8032  axrnegex  8082  axprecex  8083  rereceu  8092  recriota  8093  nntopi  8097  axcaucvglemval  8100  axcaucvglemcau  8101  cnegexlem1  8337  cnegex  8340  cnegex2  8341  subval  8354  subadd  8365  subadd2  8366  subsub23  8367  addsubeq4  8377  subcan2  8387  negcon1  8414  subcan  8417  addrsub  8533  ltadd2  8582  ltordlem  8645  recexre  8741  recexap  8816  muleqadd  8831  receuap  8832  divvalap  8837  divmulap  8838  rec11ap  8873  rerecapb  9006  zdiv  9551  uzin  9772  xaddval  10058  xnn0xadd0  10080  xnegdi  10081  xltadd1  10089  icc0r  10139  fznlem  10254  fseq1m1p1  10308  1fv  10352  fzon  10380  fvinim0ffz  10464  ioo0  10496  ico0  10498  ioc0  10499  flqbi  10527  divfl0  10533  modq0  10568  modqmuladdnn0  10607  addmodlteq  10637  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  seq3f1olemstep  10753  seq3f1olemp  10754  seq3id  10764  seq3z  10767  qsqeqor  10889  ccat0  11149  wrdl1s1  11183  ccatws1lenp1bg  11188  pfxsuff1eqwrdeq  11252  swrdccatin2  11282  pfxccatin12lem2  11284  mulreap  11396  rennim  11534  resqrexlemex  11557  rsqrmo  11559  resqrtcl  11561  rersqrtthlem  11562  sqrtsq2  11575  isumss  11923  fsum00  11994  telfsumo  11998  pwm1geoserap1  12040  prodssdc  12121  absefib  12303  efieq1re  12304  divides  12321  dvdsval2  12322  nndivides  12329  dvds0lem  12333  dvds1lem  12334  dvds2lem  12335  negdvdsb  12339  muldvds1  12348  muldvds2  12349  dvdscmulr  12352  dvdsmulcr  12353  dvdstr  12360  dvdsabseq  12379  divconjdvds  12381  odd2np1lem  12404  odd2np1  12405  even2n  12406  oddm1even  12407  2tp1odd  12416  opeo  12429  omeo  12430  m1exp1  12433  divalgb  12457  gcdaddm  12526  gcdabs1  12531  bezout  12553  gcdmultiple  12562  gcdmultiplez  12563  rplpwr  12569  rppwr  12570  nninfctlemfo  12582  alginv  12590  algcvga  12594  algfx  12595  eucalgval2  12596  coprmdvds  12635  qredeq  12639  qredeu  12640  divgcdcoprm0  12644  divgcdcoprmex  12645  cncongr1  12646  rpexp  12696  rpexp12i  12698  cncongrprm  12700  qnumdenbi  12735  phival  12756  phicl2  12757  dfphi2  12763  phiprmpw  12765  phimullem  12768  eulerthlem1  12770  eulerthlemfi  12771  eulerthlemrprm  12772  eulerthlemth  12775  eulerth  12776  fermltl  12777  hashgcdlem  12781  phisum  12784  odzval  12785  odzdvds  12789  reumodprminv  12797  modprm0  12798  nnnn0modprm0  12799  modprmn0modprm0  12800  coprimeprodsq  12801  coprimeprodsq2  12802  pythagtriplem2  12810  pythagtrip  12827  pceulem  12838  pcval  12840  pcqmul  12847  pcqcl  12850  pcabs  12870  pc2dvds  12874  pcaddlem  12883  pcadd  12884  pcmpt  12887  prmpwdvds  12899  pockthi  12902  4sqlem12  12946  ennnfonelemhf1o  13005  fvprif  13397  mgmidmo  13426  grpidvalg  13427  grpidpropdg  13428  ismgmid  13431  ismgmid2  13434  mgmidsssn0  13438  grpinvalem  13439  grprida  13441  igsumvalx  13443  gsumress  13449  ismnddef  13472  sgrpidmndm  13474  ismndd  13491  mndpropd  13494  mndinvmod  13499  mnd1  13509  ismhm  13515  gsumvallem2  13547  grpinvex  13564  isgrpd2  13575  isgrpd  13577  dfgrp2  13581  grpinveu  13592  grpinvval  13597  grplinv  13604  isgrpinv  13608  grplrinv  13611  grpidinv2  13612  grpidinv  13613  grplmulf1o  13628  grpsubeq0  13640  grpsubadd  13642  dfgrp3mlem  13652  dfgrp3m  13653  grp1  13660  imasgrp2  13668  qusgrp2  13671  mhmmnd  13674  ghmgrp  13676  mulgval  13680  mulgaddcom  13704  eqg0el  13787  ghmeqker  13829  ghmf1  13831  conjnmzb  13838  ablsubadd  13870  ablsubsub23  13883  rngmneg1  13931  rngmneg2  13932  dfur2g  13946  srgideu  13956  srgidmlem  13962  issrgid  13965  srgrz  13968  srglz  13969  srgisid  13970  srg1zr  13971  ringideu  14001  ringidmlem  14006  isringid  14009  ringid  14010  qusring2  14050  oppr0g  14065  oppr1g  14066  dvdsrvald  14078  dvdsrmuld  14081  dvdsr01  14089  dvdsr02  14090  opprunitd  14095  crngunit  14096  unitinvinv  14109  dvreq1  14127  dvdsrpropdg  14132  rhmdvdsr  14160  lringuplu  14181  subrg1  14216  subrgdvds  14220  isrrg  14248  rrgeq0i  14249  rrgeq0  14250  domneq0  14257  islmod  14276  islmodd  14278  lmodprop2d  14333  lss1d  14368  cnfldui  14574  znval  14621  znidom  14642  znunit  14644  znrrg  14645  mplelbascoe  14677  ntreq0  14827  ispsmet  15018  psmet0  15022  ismet  15039  isxmet  15040  xmeteq0  15054  metn0  15073  xmetres2  15074  xblss2ps  15099  xblss2  15100  xmseq0  15163  comet  15194  bdxmet  15196  cnmet  15225  ivthdec  15339  ivthreinc  15340  elply2  15430  reeff1o  15468  ioocosf1o  15549  logbgcd1irr  15662  logbgcd1irraplemexp  15663  mpodvdsmulf1o  15685  lgsval  15704  lgsdir  15735  lgsne0  15738  lgsprme0  15742  lgsdirnn0  15747  gausslemma2dlem0c  15751  gausslemma2dlem0i  15757  gausslemma2dlem7  15768  gausslemma2d  15769  lgseisenlem2  15771  lgseisenlem3  15772  lgsquadlem1  15777  lgsquadlem2  15778  lgsquad2lem2  15782  lgsquad3  15784  m1lgs  15785  2lgs  15804  2sqlem7  15821  2sqlem8  15823  2sqlem9  15824  edg0iedg0g  15887  upgredg  15963  ushgredgedgloop  16047  edg0usgr  16066  vtxdgfval  16074  vtxdgop  16078  vtxdeqd  16082  vtxdfifiun  16083  vtxd0nedgbfi  16085  wksfval  16094  wlklenvclwlk  16145  bj-charfunbi  16283  2omap  16472  pw1map  16474  pwle2  16477  subctctexmid  16479  peano4nninf  16486  nninfalllem1  16488  nninfsellemdc  16490  nninfsellemeq  16494  nninfsellemqall  16495  nninfsellemeqinf  16496  isomninnlem  16512  trilpolemlt1  16523  trirec0  16526  iswomninnlem  16531  iswomni0  16533  ismkvnnlem  16534  dceqnconst  16542  dcapnconst  16543