Theorem eqeq1d 2202

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 2200	. 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 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  rspcedeq1vd  2873  sbceq2g  3102  csbhypf  3119  csbiebt  3120  csbiebg  3123  dfss4st  3392  disjssun  3510  sneqrg  3788  preq12b  3796  preq12bg  3799  disji2  4022  iin0r  4198  opthg  4267  opeqsn  4281  unisucg  4445  opthreg  4588  tfisi  4619  dmsnopg  5137  relcoi1  5197  iotaeq  5223  iotabi  5224  fneq1  5342  fnun  5360  fnresdisj  5364  fnimadisj  5374  fnimaeq0  5375  sbcfng  5401  foeq1  5472  foco  5487  fveqeq2d  5562  fvelimab  5613  fvun1  5623  fvmptdv2  5647  fneqeql  5666  dffo3  5705  fvsng  5754  fconstfvm  5776  eufnfv  5789  f1veqaeq  5812  dff13f  5813  f1elima  5816  foeqcnvco  5833  f1eqcocnv  5834  acexmidlemab  5912  ovanraleqv  5942  eloprabga  6005  ovmpodv2  6052  ovi3  6055  ovelimab  6069  caovcang  6080  caovcan  6083  caovimo  6112  suppssfv  6126  suppssov1  6127  caofinvl  6155  uchoice  6190  op1stg  6203  op2ndg  6204  eqop  6230  reldm  6239  xporderlem  6284  tposfo2  6320  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  nnm0r  6532  nnmord  6570  nnaordex  6581  nnawordex  6582  ereq1  6594  eqerlem  6618  mapsn  6744  endisj  6878  pw2f1odclem  6890  xpf1o  6900  mapxpen  6904  fidifsnen  6926  supelti  7061  updjudhcoinlf  7139  updjudhcoinrg  7140  updjud  7141  omp1eomlem  7153  difinfsnlem  7158  nnnninfeq  7187  enomnilem  7197  finomni  7199  exmidomni  7201  fodjuomnilemres  7207  fodjuomni  7208  ismkvnex  7214  mkvprop  7217  fodjumkvlemres  7218  enmkvlem  7220  enwomnilem  7228  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemginf  7235  pm54.43  7250  exmidfodomrlemrALT  7263  cc2lem  7326  addnidpig  7396  ltexpi  7397  dfplpq2  7414  dfmpq2  7415  recexnq  7450  recmulnqg  7451  ltexnqq  7468  halfnqq  7470  enq0tr  7494  nqnq0pi  7498  addnnnq0  7509  addlocpr  7596  ltexprlemru  7672  ltexpri  7673  lteupri  7677  prplnqu  7680  recexpr  7698  addsrpr  7805  mulsrpr  7806  00sr  7829  negexsr  7832  recexgt0sr  7833  srpospr  7843  prsrriota  7848  caucvgsrlemfv  7851  map2psrprg  7865  elrealeu  7889  axrnegex  7939  axprecex  7940  rereceu  7949  recriota  7950  nntopi  7954  axcaucvglemval  7957  axcaucvglemcau  7958  cnegexlem1  8194  cnegex  8197  cnegex2  8198  subval  8211  subadd  8222  subadd2  8223  subsub23  8224  addsubeq4  8234  subcan2  8244  negcon1  8271  subcan  8274  addrsub  8390  ltadd2  8438  ltordlem  8501  recexre  8597  recexap  8672  muleqadd  8687  receuap  8688  divvalap  8693  divmulap  8694  rec11ap  8729  rerecapb  8862  zdiv  9405  uzin  9625  xaddval  9911  xnn0xadd0  9933  xnegdi  9934  xltadd1  9942  icc0r  9992  fznlem  10107  fseq1m1p1  10161  1fv  10205  fzon  10233  fvinim0ffz  10308  ioo0  10328  ico0  10330  ioc0  10331  flqbi  10359  divfl0  10365  modq0  10400  modqmuladdnn0  10439  addmodlteq  10469  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  seq3f1olemstep  10585  seq3f1olemp  10586  seq3id  10596  seq3z  10599  qsqeqor  10721  mulreap  11008  rennim  11146  resqrexlemex  11169  rsqrmo  11171  resqrtcl  11173  rersqrtthlem  11174  sqrtsq2  11187  isumss  11534  fsum00  11605  telfsumo  11609  pwm1geoserap1  11651  prodssdc  11732  absefib  11914  efieq1re  11915  divides  11932  dvdsval2  11933  nndivides  11940  dvds0lem  11944  dvds1lem  11945  dvds2lem  11946  negdvdsb  11950  muldvds1  11959  muldvds2  11960  dvdscmulr  11963  dvdsmulcr  11964  dvdstr  11971  dvdsabseq  11989  divconjdvds  11991  odd2np1lem  12013  odd2np1  12014  even2n  12015  oddm1even  12016  2tp1odd  12025  opeo  12038  omeo  12039  m1exp1  12042  divalgb  12066  gcdaddm  12121  gcdabs1  12126  bezout  12148  gcdmultiple  12157  gcdmultiplez  12158  rplpwr  12164  rppwr  12165  nninfctlemfo  12177  alginv  12185  algcvga  12189  algfx  12190  eucalgval2  12191  coprmdvds  12230  qredeq  12234  qredeu  12235  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  rpexp  12291  rpexp12i  12293  cncongrprm  12295  qnumdenbi  12330  phival  12351  phicl2  12352  dfphi2  12358  phiprmpw  12360  phimullem  12363  eulerthlem1  12365  eulerthlemfi  12366  eulerthlemrprm  12367  eulerthlemth  12370  eulerth  12371  fermltl  12372  hashgcdlem  12376  phisum  12378  odzval  12379  odzdvds  12383  reumodprminv  12391  modprm0  12392  nnnn0modprm0  12393  modprmn0modprm0  12394  coprimeprodsq  12395  coprimeprodsq2  12396  pythagtriplem2  12404  pythagtrip  12421  pceulem  12432  pcval  12434  pcqmul  12441  pcqcl  12444  pcabs  12464  pc2dvds  12468  pcaddlem  12477  pcadd  12478  pcmpt  12481  prmpwdvds  12493  pockthi  12496  4sqlem12  12540  ennnfonelemhf1o  12570  fvprif  12926  mgmidmo  12955  grpidvalg  12956  grpidpropdg  12957  ismgmid  12960  ismgmid2  12963  mgmidsssn0  12967  grpinvalem  12968  grprida  12970  igsumvalx  12972  gsumress  12978  ismnddef  12999  sgrpidmndm  13001  ismndd  13018  mndpropd  13021  mndinvmod  13026  mnd1  13027  ismhm  13033  gsumvallem2  13065  grpinvex  13082  isgrpd2  13093  isgrpd  13095  dfgrp2  13099  grpinveu  13110  grpinvval  13115  grplinv  13122  isgrpinv  13126  grplrinv  13129  grpidinv2  13130  grpidinv  13131  grplmulf1o  13146  grpsubeq0  13158  grpsubadd  13160  dfgrp3mlem  13170  dfgrp3m  13171  grp1  13178  imasgrp2  13180  qusgrp2  13183  mhmmnd  13186  ghmgrp  13188  mulgval  13192  mulgaddcom  13216  eqg0el  13299  ghmeqker  13341  ghmf1  13343  conjnmzb  13350  ablsubadd  13382  ablsubsub23  13395  rngmneg1  13443  rngmneg2  13444  dfur2g  13458  srgideu  13468  srgidmlem  13474  issrgid  13477  srgrz  13480  srglz  13481  srgisid  13482  srg1zr  13483  ringideu  13513  ringidmlem  13518  isringid  13521  ringid  13522  qusring2  13562  oppr0g  13577  oppr1g  13578  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrmuld  13592  dvdsr01  13600  dvdsr02  13601  opprunitd  13606  crngunit  13607  unitinvinv  13620  dvreq1  13638  dvdsrpropdg  13643  rhmdvdsr  13671  lringuplu  13692  subrg1  13727  subrgdvds  13731  isrrg  13759  rrgeq0i  13760  rrgeq0  13761  domneq0  13768  islmod  13787  islmodd  13789  lmodprop2d  13844  lss1d  13879  cnfldui  14077  znval  14124  znidom  14145  znunit  14147  znrrg  14148  ntreq0  14300  ispsmet  14491  psmet0  14495  ismet  14512  isxmet  14513  xmeteq0  14527  metn0  14546  xmetres2  14547  xblss2ps  14572  xblss2  14573  xmseq0  14636  comet  14667  bdxmet  14669  cnmet  14698  ivthdec  14798  ivthreinc  14799  elply2  14881  reeff1o  14908  ioocosf1o  14989  logbgcd1irr  15099  logbgcd1irraplemexp  15100  lgsval  15120  lgsdir  15151  lgsne0  15154  lgsprme0  15158  lgsdirnn0  15163  gausslemma2dlem0c  15167  gausslemma2dlem0i  15173  gausslemma2dlem7  15184  gausslemma2d  15185  lgseisenlem2  15187  lgseisenlem3  15188  lgsquadlem1  15191  m1lgs  15192  2sqlem7  15208  2sqlem8  15210  2sqlem9  15211  bj-charfunbi  15303  pwle2  15489  subctctexmid  15491  peano4nninf  15496  nninfalllem1  15498  nninfsellemdc  15500  nninfsellemeq  15504  nninfsellemqall  15505  nninfsellemeqinf  15506  isomninnlem  15520  trilpolemlt1  15531  trirec0  15534  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  dceqnconst  15550  dcapnconst  15551