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  2851  sbceq2g  3080  csbhypf  3096  csbiebt  3097  csbiebg  3100  dfss4st  3369  disjssun  3487  sneqrg  3763  preq12b  3771  preq12bg  3774  disji2  3997  iin0r  4170  opthg  4239  opeqsn  4253  unisucg  4415  opthreg  4556  tfisi  4587  dmsnopg  5101  relcoi1  5161  iotaeq  5187  iotabi  5188  fneq1  5305  fnun  5323  fnresdisj  5327  fnimadisj  5337  fnimaeq0  5338  sbcfng  5364  foeq1  5435  foco  5449  fveqeq2d  5524  fvelimab  5573  fvun1  5583  fvmptdv2  5606  fneqeql  5625  dffo3  5664  fvsng  5713  fconstfvm  5735  eufnfv  5748  f1veqaeq  5770  dff13f  5771  f1elima  5774  foeqcnvco  5791  f1eqcocnv  5792  acexmidlemab  5869  ovanraleqv  5899  eloprabga  5962  ovmpodv2  6008  ovi3  6011  ovelimab  6025  caovcang  6036  caovcan  6039  caovimo  6068  suppssfv  6079  suppssov1  6080  caofinvl  6105  op1stg  6151  op2ndg  6152  eqop  6178  reldm  6187  xporderlem  6232  tposfo2  6268  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  nnm0r  6480  nnmord  6518  nnaordex  6529  nnawordex  6530  ereq1  6542  eqerlem  6566  mapsn  6690  endisj  6824  xpf1o  6844  mapxpen  6848  fidifsnen  6870  supelti  7001  updjudhcoinlf  7079  updjudhcoinrg  7080  updjud  7081  omp1eomlem  7093  difinfsnlem  7098  nnnninfeq  7126  enomnilem  7136  finomni  7138  exmidomni  7140  fodjuomnilemres  7146  fodjuomni  7147  ismkvnex  7153  mkvprop  7156  fodjumkvlemres  7157  enmkvlem  7159  enwomnilem  7167  nninfdcinf  7169  nninfwlporlem  7171  nninfwlpoimlemginf  7174  pm54.43  7189  exmidfodomrlemrALT  7202  cc2lem  7265  addnidpig  7335  ltexpi  7336  dfplpq2  7353  dfmpq2  7354  recexnq  7389  recmulnqg  7390  ltexnqq  7407  halfnqq  7409  enq0tr  7433  nqnq0pi  7437  addnnnq0  7448  addlocpr  7535  ltexprlemru  7611  ltexpri  7612  lteupri  7616  prplnqu  7619  recexpr  7637  addsrpr  7744  mulsrpr  7745  00sr  7768  negexsr  7771  recexgt0sr  7772  srpospr  7782  prsrriota  7787  caucvgsrlemfv  7790  map2psrprg  7804  elrealeu  7828  axrnegex  7878  axprecex  7879  rereceu  7888  recriota  7889  nntopi  7893  axcaucvglemval  7896  axcaucvglemcau  7897  cnegexlem1  8132  cnegex  8135  cnegex2  8136  subval  8149  subadd  8160  subadd2  8161  subsub23  8162  addsubeq4  8172  subcan2  8182  negcon1  8209  subcan  8212  addrsub  8328  ltadd2  8376  ltordlem  8439  recexre  8535  recexap  8610  muleqadd  8625  receuap  8626  divvalap  8631  divmulap  8632  rec11ap  8667  rerecapb  8800  zdiv  9341  uzin  9560  xaddval  9845  xnn0xadd0  9867  xnegdi  9868  xltadd1  9876  icc0r  9926  fznlem  10041  fseq1m1p1  10095  1fv  10139  fzon  10166  fvinim0ffz  10241  ioo0  10260  ico0  10262  ioc0  10263  flqbi  10290  divfl0  10296  modq0  10329  modqmuladdnn0  10368  addmodlteq  10398  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  seq3f1olemstep  10501  seq3f1olemp  10502  seq3id  10508  seq3z  10511  qsqeqor  10631  mulreap  10873  rennim  11011  resqrexlemex  11034  rsqrmo  11036  resqrtcl  11038  rersqrtthlem  11039  sqrtsq2  11052  isumss  11399  fsum00  11470  telfsumo  11474  pwm1geoserap1  11516  prodssdc  11597  absefib  11778  efieq1re  11779  divides  11796  dvdsval2  11797  nndivides  11804  dvds0lem  11808  dvds1lem  11809  dvds2lem  11810  negdvdsb  11814  muldvds1  11823  muldvds2  11824  dvdscmulr  11827  dvdsmulcr  11828  dvdstr  11835  dvdsabseq  11853  divconjdvds  11855  odd2np1lem  11877  odd2np1  11878  even2n  11879  oddm1even  11880  2tp1odd  11889  opeo  11902  omeo  11903  m1exp1  11906  divalgb  11930  gcdaddm  11985  gcdabs1  11990  bezout  12012  gcdmultiple  12021  gcdmultiplez  12022  rplpwr  12028  rppwr  12029  alginv  12047  algcvga  12051  algfx  12052  eucalgval2  12053  coprmdvds  12092  qredeq  12096  qredeu  12097  divgcdcoprm0  12101  divgcdcoprmex  12102  cncongr1  12103  rpexp  12153  rpexp12i  12155  cncongrprm  12157  qnumdenbi  12192  phival  12213  phicl2  12214  dfphi2  12220  phiprmpw  12222  phimullem  12225  eulerthlem1  12227  eulerthlemfi  12228  eulerthlemrprm  12229  eulerthlemth  12232  eulerth  12233  fermltl  12234  hashgcdlem  12238  phisum  12240  odzval  12241  odzdvds  12245  reumodprminv  12253  modprm0  12254  nnnn0modprm0  12255  modprmn0modprm0  12256  coprimeprodsq  12257  coprimeprodsq2  12258  pythagtriplem2  12266  pythagtrip  12283  pceulem  12294  pcval  12296  pcqmul  12303  pcqcl  12306  pcabs  12325  pc2dvds  12329  pcaddlem  12338  pcadd  12339  pcmpt  12341  prmpwdvds  12353  pockthi  12356  ennnfonelemhf1o  12414  fvprif  12762  mgmidmo  12791  grpidvalg  12792  grpidpropdg  12793  ismgmid  12796  ismgmid2  12799  mgmidsssn0  12803  grprinvlem  12804  grpridd  12806  ismnddef  12819  sgrpidmndm  12821  ismndd  12838  mndpropd  12841  mndinvmod  12846  mnd1  12847  ismhm  12853  grpinvex  12887  isgrpd2  12897  isgrpd  12899  dfgrp2  12902  grpinveu  12911  grpinvval  12916  grplinv  12922  isgrpinv  12926  grplrinv  12927  grpidinv2  12928  grpidinv  12929  grplmulf1o  12944  grpsubeq0  12956  grpsubadd  12958  dfgrp3mlem  12968  dfgrp3m  12969  grp1  12976  mhmmnd  12980  ghmgrp  12982  mulgval  12986  mulgaddcom  13007  ablsubadd  13115  ablsubsub23  13128  dfur2g  13145  srgideu  13155  srgidmlem  13161  issrgid  13164  srgrz  13167  srglz  13168  srgisid  13169  srg1zr  13170  ringideu  13200  ringidmlem  13205  isringid  13208  ringid  13209  oppr0g  13251  oppr1g  13252  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrmuld  13265  dvdsr01  13273  dvdsr02  13274  opprunitd  13279  crngunit  13280  unitinvinv  13293  dvreq1  13311  dvdsrpropdg  13316  lringuplu  13337  subrg1  13352  subrgdvds  13356  islmod  13381  islmodd  13383  lmodprop2d  13438  ntreq0  13635  ispsmet  13826  psmet0  13830  ismet  13847  isxmet  13848  xmeteq0  13862  metn0  13881  xmetres2  13882  xblss2ps  13907  xblss2  13908  xmseq0  13971  comet  14002  bdxmet  14004  cnmet  14033  ivthdec  14125  reeff1o  14197  ioocosf1o  14278  logbgcd1irr  14388  logbgcd1irraplemexp  14389  lgsval  14408  lgsdir  14439  lgsne0  14442  lgsprme0  14446  lgsdirnn0  14451  lgseisenlem2  14454  m1lgs  14455  2sqlem7  14471  2sqlem8  14473  2sqlem9  14474  bj-charfunbi  14566  pwle2  14751  subctctexmid  14753  peano4nninf  14758  nninfalllem1  14760  nninfsellemdc  14762  nninfsellemeq  14766  nninfsellemqall  14767  nninfsellemeqinf  14768  isomninnlem  14781  trilpolemlt1  14792  trirec0  14795  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803  dceqnconst  14810  dcapnconst  14811