Theorem eqeq1d 2186

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 2184	. 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 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  rspcedeq1vd  2852  sbceq2g  3081  csbhypf  3097  csbiebt  3098  csbiebg  3101  dfss4st  3370  disjssun  3488  sneqrg  3764  preq12b  3772  preq12bg  3775  disji2  3998  iin0r  4171  opthg  4240  opeqsn  4254  unisucg  4416  opthreg  4557  tfisi  4588  dmsnopg  5102  relcoi1  5162  iotaeq  5188  iotabi  5189  fneq1  5306  fnun  5324  fnresdisj  5328  fnimadisj  5338  fnimaeq0  5339  sbcfng  5365  foeq1  5436  foco  5450  fveqeq2d  5525  fvelimab  5574  fvun1  5584  fvmptdv2  5607  fneqeql  5626  dffo3  5665  fvsng  5714  fconstfvm  5736  eufnfv  5749  f1veqaeq  5772  dff13f  5773  f1elima  5776  foeqcnvco  5793  f1eqcocnv  5794  acexmidlemab  5871  ovanraleqv  5901  eloprabga  5964  ovmpodv2  6010  ovi3  6013  ovelimab  6027  caovcang  6038  caovcan  6041  caovimo  6070  suppssfv  6081  suppssov1  6082  caofinvl  6107  op1stg  6153  op2ndg  6154  eqop  6180  reldm  6189  xporderlem  6234  tposfo2  6270  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  nnm0r  6482  nnmord  6520  nnaordex  6531  nnawordex  6532  ereq1  6544  eqerlem  6568  mapsn  6692  endisj  6826  xpf1o  6846  mapxpen  6850  fidifsnen  6872  supelti  7003  updjudhcoinlf  7081  updjudhcoinrg  7082  updjud  7083  omp1eomlem  7095  difinfsnlem  7100  nnnninfeq  7128  enomnilem  7138  finomni  7140  exmidomni  7142  fodjuomnilemres  7148  fodjuomni  7149  ismkvnex  7155  mkvprop  7158  fodjumkvlemres  7159  enmkvlem  7161  enwomnilem  7169  nninfdcinf  7171  nninfwlporlem  7173  nninfwlpoimlemginf  7176  pm54.43  7191  exmidfodomrlemrALT  7204  cc2lem  7267  addnidpig  7337  ltexpi  7338  dfplpq2  7355  dfmpq2  7356  recexnq  7391  recmulnqg  7392  ltexnqq  7409  halfnqq  7411  enq0tr  7435  nqnq0pi  7439  addnnnq0  7450  addlocpr  7537  ltexprlemru  7613  ltexpri  7614  lteupri  7618  prplnqu  7621  recexpr  7639  addsrpr  7746  mulsrpr  7747  00sr  7770  negexsr  7773  recexgt0sr  7774  srpospr  7784  prsrriota  7789  caucvgsrlemfv  7792  map2psrprg  7806  elrealeu  7830  axrnegex  7880  axprecex  7881  rereceu  7890  recriota  7891  nntopi  7895  axcaucvglemval  7898  axcaucvglemcau  7899  cnegexlem1  8134  cnegex  8137  cnegex2  8138  subval  8151  subadd  8162  subadd2  8163  subsub23  8164  addsubeq4  8174  subcan2  8184  negcon1  8211  subcan  8214  addrsub  8330  ltadd2  8378  ltordlem  8441  recexre  8537  recexap  8612  muleqadd  8627  receuap  8628  divvalap  8633  divmulap  8634  rec11ap  8669  rerecapb  8802  zdiv  9343  uzin  9562  xaddval  9847  xnn0xadd0  9869  xnegdi  9870  xltadd1  9878  icc0r  9928  fznlem  10043  fseq1m1p1  10097  1fv  10141  fzon  10168  fvinim0ffz  10243  ioo0  10262  ico0  10264  ioc0  10265  flqbi  10292  divfl0  10298  modq0  10331  modqmuladdnn0  10370  addmodlteq  10400  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  seq3f1olemstep  10503  seq3f1olemp  10504  seq3id  10510  seq3z  10513  qsqeqor  10633  mulreap  10875  rennim  11013  resqrexlemex  11036  rsqrmo  11038  resqrtcl  11040  rersqrtthlem  11041  sqrtsq2  11054  isumss  11401  fsum00  11472  telfsumo  11476  pwm1geoserap1  11518  prodssdc  11599  absefib  11780  efieq1re  11781  divides  11798  dvdsval2  11799  nndivides  11806  dvds0lem  11810  dvds1lem  11811  dvds2lem  11812  negdvdsb  11816  muldvds1  11825  muldvds2  11826  dvdscmulr  11829  dvdsmulcr  11830  dvdstr  11837  dvdsabseq  11855  divconjdvds  11857  odd2np1lem  11879  odd2np1  11880  even2n  11881  oddm1even  11882  2tp1odd  11891  opeo  11904  omeo  11905  m1exp1  11908  divalgb  11932  gcdaddm  11987  gcdabs1  11992  bezout  12014  gcdmultiple  12023  gcdmultiplez  12024  rplpwr  12030  rppwr  12031  alginv  12049  algcvga  12053  algfx  12054  eucalgval2  12055  coprmdvds  12094  qredeq  12098  qredeu  12099  divgcdcoprm0  12103  divgcdcoprmex  12104  cncongr1  12105  rpexp  12155  rpexp12i  12157  cncongrprm  12159  qnumdenbi  12194  phival  12215  phicl2  12216  dfphi2  12222  phiprmpw  12224  phimullem  12227  eulerthlem1  12229  eulerthlemfi  12230  eulerthlemrprm  12231  eulerthlemth  12234  eulerth  12235  fermltl  12236  hashgcdlem  12240  phisum  12242  odzval  12243  odzdvds  12247  reumodprminv  12255  modprm0  12256  nnnn0modprm0  12257  modprmn0modprm0  12258  coprimeprodsq  12259  coprimeprodsq2  12260  pythagtriplem2  12268  pythagtrip  12285  pceulem  12296  pcval  12298  pcqmul  12305  pcqcl  12308  pcabs  12327  pc2dvds  12331  pcaddlem  12340  pcadd  12341  pcmpt  12343  prmpwdvds  12355  pockthi  12358  ennnfonelemhf1o  12416  fvprif  12767  mgmidmo  12796  grpidvalg  12797  grpidpropdg  12798  ismgmid  12801  ismgmid2  12804  mgmidsssn0  12808  grprinvlem  12809  grpridd  12811  ismnddef  12824  sgrpidmndm  12826  ismndd  12843  mndpropd  12846  mndinvmod  12851  mnd1  12852  ismhm  12858  grpinvex  12892  isgrpd2  12902  isgrpd  12904  dfgrp2  12907  grpinveu  12916  grpinvval  12921  grplinv  12927  isgrpinv  12931  grplrinv  12932  grpidinv2  12933  grpidinv  12934  grplmulf1o  12949  grpsubeq0  12961  grpsubadd  12963  dfgrp3mlem  12973  dfgrp3m  12974  grp1  12981  mhmmnd  12985  ghmgrp  12987  mulgval  12991  mulgaddcom  13012  ablsubadd  13120  ablsubsub23  13133  dfur2g  13150  srgideu  13160  srgidmlem  13166  issrgid  13169  srgrz  13172  srglz  13173  srgisid  13174  srg1zr  13175  ringideu  13205  ringidmlem  13210  isringid  13213  ringid  13214  oppr0g  13256  oppr1g  13257  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrmuld  13270  dvdsr01  13278  dvdsr02  13279  opprunitd  13284  crngunit  13285  unitinvinv  13298  dvreq1  13316  dvdsrpropdg  13321  lringuplu  13342  subrg1  13357  subrgdvds  13361  islmod  13386  islmodd  13388  lmodprop2d  13443  lss1d  13475  ntreq0  13671  ispsmet  13862  psmet0  13866  ismet  13883  isxmet  13884  xmeteq0  13898  metn0  13917  xmetres2  13918  xblss2ps  13943  xblss2  13944  xmseq0  14007  comet  14038  bdxmet  14040  cnmet  14069  ivthdec  14161  reeff1o  14233  ioocosf1o  14314  logbgcd1irr  14424  logbgcd1irraplemexp  14425  lgsval  14444  lgsdir  14475  lgsne0  14478  lgsprme0  14482  lgsdirnn0  14487  lgseisenlem2  14490  m1lgs  14491  2sqlem7  14507  2sqlem8  14509  2sqlem9  14510  bj-charfunbi  14602  pwle2  14787  subctctexmid  14789  peano4nninf  14794  nninfalllem1  14796  nninfsellemdc  14798  nninfsellemeq  14802  nninfsellemqall  14803  nninfsellemeqinf  14804  isomninnlem  14817  trilpolemlt1  14828  trirec0  14831  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839  dceqnconst  14846  dcapnconst  14847